Structures · Algebra
NonUnitalNonAssocRing
A not-necessarily-unital, not-necessarily-associative ring.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds left_distrib, right_distrib, zero_mul, mul_zero
Extends2
Extended by6
Forgetful instances
Every NonUnitalNonAssocRing is also a
Concrete types that are instances28
- SeparationQuotient
- Filter.Germ
- CStarMatrix
- TensorProduct
- WithConv
- Matrix
- HahnSeries
- LocallyConstant
- FreeAbelianGroup
- MonoidAlgebra
- AddMonoidAlgebra
- DirectLimit
- Finsupp
- DirectSum
- SkewMonoidAlgebra
- ZeroAtInftyContinuousMap
- RingCon.Quotient
- CompactlySupportedContinuousMap
- CommutatorRing
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
How is a type an instance?
Loading the hierarchy index…
Assumed by476
- mul_sub
- sub_mul
- TwoSidedIdeal.ringCon
- NonUnitalNonAssocRing.toMul
- NonUnitalSubring.closure
- NonUnitalSubring.map
- RingSeminorm.toAddGroupSeminorm
- NonUnitalSubring.comap
- NonUnitalSubring.toNonUnitalSubsemiring
- associator
- NonUnitalSubring.center
- NonUnitalRingHom.range
- RingNorm.toRingSeminorm
- NonUnitalSubring.toAddSubgroup
- TwoSidedIdeal.matrix
- mul_sub_left_distrib
- TwoSidedIdeal.span
- NonUnitalSubalgebra.toNonUnitalSubring
- NonUnitalSubring.subset_closure
- Commute.sub_left
- TwoSidedIdeal.mem_iff
- NonUnitalSubring.prod
- Matrix.neg_mul
- TwoSidedIdeal.mk'
- TwoSidedIdeal.mul_mem_left
- NonUnitalSubring.toSubsemigroup
- NonUnitalSubring.gc_map_comap
- NonUnitalSubring.closure_le
- TwoSidedIdeal.mul_mem_right
- NonUnitalSubring.gi
- NonUnitalSubringClass.subtype
- Commute.sub_right
- dotProduct_neg
- NonUnitalSubring.mk'
- TwoSidedIdeal.ker
- TwoSidedIdeal.mem_span_iff
- neg_dotProduct
- TwoSidedIdeal.comap
- Ring.lie_def
- Matrix.mul_neg
- RingEquiv.mapTwoSidedIdeal
- TwoSidedIdeal.zero_mem
- TwoSidedIdeal.coe_mk'
- TwoSidedIdeal.op
- TwoSidedIdeal.rel_iff
- TwoSidedIdeal.orderIsoRingCon
- TwoSidedIdeal.unop
- TwoSidedIdeal.subset_span
- mul_sub_right_distrib
- Commute.mul_self_sub_mul_self_eq
Ancestors52
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Bracket
- 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
- NonUnitalNonAssocSemiring
- Nonempty
- OfNat
- One
- SMul
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero