Structures · Algebra
NonUnitalNonAssocCommRing
A non-unital non-associative commutative ring is a NonUnitalNonAssocRing with commutative
multiplication.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds mul_comm
Extends2
Extended by2
Concrete types that are instances5
- SeparationQuotient
- WithConv
- DirectLimit
- RingCon.Quotient
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- mul_self_eq_mul_self_iff
- DirectLimit.instNonUnitalNonAssocCommRingOfNonUnitalRingHomClass
- NonUnitalNonAssocCommRing.mul_comm
- NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring
- Function.Surjective.nonUnitalNonAssocCommRing
- RingCon.instNonUnitalNonAssocCommRingQuotient
- NonUnitalSubringClass.toNonUnitalNonAssocCommRing
- Function.Injective.nonUnitalNonAssocCommRing
- NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
- two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add
- mul_self_sub_mul_self
- two_nsmul_lie_lmul_lmul_add_add_eq_zero
- SeparationQuotient.instNonUnitalNonAssocCommRing
- instNonUnitalNonAssocCommRingWithConvMatrix
Ancestors55
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Bracket
- CommMagma
- Distrib
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Mul
- MulZeroClass
- NSMul
- Neg
- NegZeroClass
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- Nonempty
- OfNat
- One
- SMul
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero