Structures · Algebra
LeftDistribClass
A typeclass stating that multiplication is left distributive over addition.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds left_distrib
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- SeparationQuotient
- Ordinal
- OrderType
- OrderDual
- Lex
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- mul_add
- dvd_add
- left_distrib
- mul_add_one
- mul_one_add
- Dvd.dvd.add
- Even.mul_left
- LeftDistribClass.left_distrib
- Matrix.vecMulVec_add
- Function.Injective.leftDistribClass
- Function.Surjective.leftDistribClass
- Lex.instLeftDistribClass
- SeparationQuotient.instLeftDistribClass
- OrderDual.instLeftDistribClass
- WithZero.instLeftDistribClass
Ancestors0
No ancestors.