Structures · Algebra
NonUnitalCommRing
A non-unital commutative ring is a NonUnitalRing with commutative multiplication.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds mul_comm
Extends2
Extended by3
Forgetful instances
Concrete types that are instances31
- Complex
- SeparationQuotient
- Filter.Germ
- UInt64
- UInt8
- UInt16
- UInt32
- WithConv
- HahnSeries
- LocallyConstant
- USize
- MeasureTheory.SimpleFunc
- MonoidAlgebra
- AddMonoidAlgebra
- DirectLimit
- Finsupp
- ContinuousMapZero
- ZeroAtInftyContinuousMap
- RingCon.Quotient
- AsBoolRing
- CompactlySupportedContinuousMap
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Fin
- Lex
- AddOpposite
- ContinuousMap
- Shrink
How is a type an instance?
Loading the hierarchy index…
Assumed by40
- dvd_mul_sub_mul
- NonUnitalSubringClass.toNonUnitalCommRing
- Prod.instNonUnitalCommRing
- instNonUnitalCommRingWithConvMatrix
- NonUnitalSubalgebra.toNonUnitalCommRing
- RingCon.instNonUnitalCommRingQuotient
- LocallyConstant.instNonUnitalCommRing
- Filter.Germ.instNonUnitalCommRing
- MeasureTheory.SimpleFunc.instNonUnitalCommRing
- ContinuousMap.instNonUnitalCommRingOfIsTopologicalRing
- ZeroAtInftyContinuousMap.instNonUnitalCommRing
- Shrink.instNonUnitalCommRing
- NonUnitalCommRing.toNonUnitalRing
- Equiv.nonUnitalCommRing
- Function.Surjective.nonUnitalCommRing
- Pi.nonUnitalCommRing
- NonUnitalNormedCommRing.induced
- selfAdjoint.val_mul
- Finsupp.instNonUnitalCommRing
- CompactlySupportedContinuousMap.instNonUnitalCommRingOfIsTopologicalRing
- NonUnitalSeminormedCommRing.induced
- NonUnitalCommRing.toNonUnitalCommSemiring
- vieta_formula_quadratic
- ULift.nonUnitalCommRing
- instCommRingCorner
- NonUnitalSubring.toNonUnitalCommRing
- NonUnitalCommRing.toNonUnitalNonAssocCommRing
- SeparationQuotient.instNonUnitalCommRing
- Lex.instNonUnitalCommRing
- DirectLimit.instNonUnitalCommRingOfNonUnitalRingHomClass
- HahnSeries.instNonUnitalCommRing
- MulOpposite.instNonUnitalCommRing
- Unitization.instCommRing
- AddOpposite.instNonUnitalCommRing
- NonUnitalCommRing.mul_comm
- Function.Injective.nonUnitalCommRing
- selfAdjoint.instMulSubtypeMemAddSubgroup
- NonUnitalStarSubalgebra.toNonUnitalCommRing
- NonUnitalSubring.center_eq_top
- OrderDual.instNonUnitalCommRing
Ancestors63
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Bracket
- CommMagma
- CommSemigroup
- Distrib
- Dvd
- 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
- NonUnitalCommSemiring
- NonUnitalNonAssocCommRing
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalRing
- NonUnitalSemiring
- Nonempty
- OfNat
- One
- SMul
- Semigroup
- SemigroupWithZero
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero