Structures · Algebra
Distrib
A typeclass stating that multiplication is left and right distributive over addition.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds left_distrib, right_distrib
Extends2
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances21
- Int
- Nat
- SeparationQuotient
- Filter.Germ
- HahnSeries
- LocallyConstant
- FreeAbelianGroup
- Zsqrtd
- PNat
- Tropical
- FreeAlgebra
- PosNum
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Fin
- Lex
- AddOpposite
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by42
- Commute.add_left
- Commute.add_right
- SemiconjBy.add_left
- SemiconjBy.add_right
- AddHom.mulLeft
- AddHom.mulRight
- Holor.mul_left_distrib
- le_mul_tsub
- Distrib.left_distrib
- Filter.mul_add_subset
- Set.add_mem_center
- Distrib.leftDistribClass
- Lex.instDistrib
- Matrix.add_kronecker
- MulOpposite.instDistrib
- Matrix.kronecker_add
- LocallyConstant.instDistrib
- Holor.mul_right_distrib
- Set.mul_add_subset
- SeparationQuotient.instDistrib
- Filter.add_mul_subset
- Distrib.toMul
- Function.Surjective.distrib
- WithZero.instDistrib
- AddHom.mulLeft_apply
- Distrib.rightDistribClass
- Finset.add_mul_subset
- Function.Injective.distrib
- AddHom.mulRight_apply
- Set.add_mem_centralizer
- AddOpposite.instDistrib
- Matrix.hadamard_add
- Filter.Germ.instDistrib
- Set.add_mul_subset
- Finset.mul_add_subset
- ULift.distrib
- Distrib.toAdd
- Matrix.add_hadamard
- Prod.instDistrib
- Pi.distrib
- OrderDual.instDistrib
- Distrib.right_distrib