Structures · Algebra
NonAssocCommRing
A non-associative commutative ring is a NonAssocRing with commutative multiplication.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds mul_comm
Extends3
Extended by1
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 by10
- NonAssocCommRing.mul_comm
- Function.Surjective.nonAssocCommRing
- instNonAssocCommRingWithConvMatrix
- NonAssocCommRing.toNonAssocCommSemiring
- NonAssocCommRing.toNonAssocRing
- Function.Injective.nonAssocCommRing
- RingCon.instNonAssocCommRingQuotient
- NonAssocCommRing.toNonUnitalNonAssocCommRing
- DirectLimit.instNonAssocCommRingOfRingHomClass
- SubringClass.toNonAssocCommRing
Ancestors68
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommGroupWithOne
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddGroup
- AddGroupWithOne
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddMonoidWithOne
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Bracket
- CommMagma
- Distrib
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- IntCast
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Mul
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NSMul
- NatCast
- Neg
- NegZeroClass
- NonAssocCommSemiring
- NonAssocRing
- NonAssocSemiring
- NonUnitalNonAssocCommRing
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- Nonempty
- OfNat
- One
- SMul
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero