17.4. The non-unital, non-associative case🔗

Since Algebra R S assumes R is a commutative semiring and S is a semiring, in the non-unital and/or non-associative case we need to replace the assumption [Algebra R S] with [Module R S] [SMulCommClass R S S] [IsScalarTower R S S]. Note that we lose access to algebraMap, so working with non-unital, non-associative ring extensions requires explicitly passing around the maps.

Given an Algebra R S instance, the instances for Module R S, SMulCommClass R S S and IsScalarTower R S S can be automatically inferred. The converse cannot be done using the typeclass system but can be added manually, using Algebra.ofModule (R := R) (A := S) smul_mul_assoc mul_smul_comm. Mathlib always uses Algebra in the unital, associative case.