Structures · Algebra
RightDistribClass
A typeclass stating that multiplication is right distributive over addition.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds right_distrib
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- SeparationQuotient
- OrderDual
- Lex
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- add_mul
- right_distrib
- add_one_mul
- one_add_mul
- Even.mul_right
- RightDistribClass.right_distrib
- Function.Surjective.rightDistribClass
- WithZero.instRightDistribClass
- Matrix.add_vecMulVec
- OrderDual.instRightDistribClass
- SeparationQuotient.instRightDistribClass
- Function.Injective.rightDistribClass
- Lex.instRightDistribClass
- distrib_three_right
Ancestors0
No ancestors.