Structures · Algebra
NonUnitalNonAssocCommSemiring
A not-necessarily-unital, not-necessarily-associative, but commutative semiring.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds mul_comm
Extends2
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances5
- SeparationQuotient
- WithConv
- DirectLimit
- RingCon.Quotient
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- LinearMap.flip_mul
- LinearMap.mul'_comp_comm
- AddMonoid.End.mulRight_eq_mulLeft
- Matrix.commute_diagonal
- NonUnitalSubsemiringClass.toNonUnitalNonAssocCommSemiring
- SeparationQuotient.instNonUnitalNonAssocCommSemiring
- instNonUnitalNonAssocCommSemiringWithConvMatrix
- NonUnitalNonAssocCommSemiring.mem_center_iff
- RingCon.instNonUnitalNonAssocCommSemiringQuotient
- NonUnitalNonAssocCommSemiring.mul_comm
- Function.Injective.nonUnitalNonAssocCommSemiring
- Function.Surjective.nonUnitalNonAssocCommSemiring
- DirectLimit.instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass
- NonUnitalNonAssocCommSemiring.toCommMagma
- NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring
- LinearMap.mul'_comm