Structures · Algebra
NonAssocCommSemiring
A non-associative commutative semiring is a NonAssocSemiring with commutative
multiplication.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds mul_comm
Extends2
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances4
- WithConv
- DirectLimit
- RingCon.Quotient
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by9
- NonAssocCommSemiring.toNonAssocSemiring
- Function.Surjective.nonAssocCommSemiring
- NonAssocCommSemiring.mul_comm
- instNonAssocCommSemiringWithConvMatrix
- Function.Injective.nonAssocCommSemiring
- RingCon.instNonAssocCommSemiringQuotient
- DirectLimit.instNonAssocCommSemiringOfRingHomClass
- SubsemiringClass.toNonAssocCommSemiring
- NonAssocCommSemiring.toNonUnitalNonAssocCommSemiring
Ancestors37
- Add
- AddAction
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddMonoid
- AddMonoidWithOne
- AddSemigroup
- AddSemigroupAction
- AddZero
- AddZeroClass
- CommMagma
- Distrib
- HAdd
- HMul
- HSMul
- HVAdd
- Lean.Grind.AddCommMonoid
- Lean.Grind.NatModule
- Mul
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NSMul
- NatCast
- NonAssocSemiring
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocSemiring
- Nonempty
- OfNat
- One
- SMul
- VAdd
- ZSMul
- Zero