Structures · Algebra
NonUnitalNonAssocSemiring
A not-necessarily-unital, not-necessarily-associative semiring. See CommutatorRing and the
documentation thereof in case you need a NonUnitalNonAssocSemiring instance on a Lie ring
or a Lie algebra.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds left_distrib, right_distrib, zero_mul, mul_zero
Extends3
Extended by4
Concrete types that are instances33
- Nat
- SeparationQuotient
- Filter.Germ
- CStarMatrix
- TensorProduct
- WithConv
- Matrix
- HahnSeries
- LocallyConstant
- QuadraticAlgebra
- MeasureTheory.SimpleFunc
- MonoidAlgebra
- AddMonoidAlgebra
- DirectLimit
- Finsupp
- DirectSum
- SkewMonoidAlgebra
- PiTensorProduct
- ZeroAtInftyContinuousMap
- SetSemiring
- RingCon.Quotient
- CompactlySupportedContinuousMap
- IncidenceAlgebra
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- WithTop
How is a type an instance?
Loading the hierarchy index…
Assumed by1,442
- Matrix.mulVec
- Finset.mul_sum
- Matrix.vecMul
- Finset.sum_mul
- NonUnitalAlgHomClass
- LinearMap.mul
- NonUnitalSubsemiring.toAddSubmonoid
- LinearMap.mul'
- Summable.mul_left
- NonUnitalStarAlgHom.comp
- WeakDual.characterSpace
- NonUnitalRingHom.comp
- NonUnitalStarSubalgebra.toNonUnitalSubalgebra
- Matrix.SeparatingRight
- LinearMap.mulLeft
- Matrix.SeparatingLeft
- NonUnitalSubalgebra.toNonUnitalSubsemiring
- NonUnitalAlgebra.adjoin
- NonUnitalSubsemiring.closure
- NonUnitalRingHomClass.toNonUnitalRingHom
- LinearMap.mul_apply_apply
- HasSum.mul_left
- LinearMap.mulRight
- QuadraticMap.sq
- RingEquiv.ofBijective
- NonUnitalStarAlgHom.range
- AddMonoidHom.mulLeft
- NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom
- Matrix.mulVec_single
- NonUnitalStarSubalgebra.map
- NonUnitalSubalgebra.toSubmodule
- NonUnitalSubalgebra.map
- NonUnitalSubsemiring.map
- NonUnitalSubsemiring.center
- NonUnitalAlgHom.comp
- AddMonoidHom.mulRight
- NonUnitalRingHom.id
- AddSubmonoid.mul
- NonUnitalRingHom.srange
- Matrix.zero_mul
- Matrix.mul_diagonal
- NonUnitalRingHom.toMulHom
- NonUnitalAlgHom.toDistribMulActionHom
- Matrix.mul_zero
- tsub_mul
- NonUnitalSubsemiring.comap
- Finset.sum_mul_sum
- NonUnitalAlgebra.subset_adjoin
- NonUnitalStarAlgHom.id
- NonUnitalSubalgebra.inclusion