Structures · Algebra
NonAssocRing
A unital but not-necessarily-associative ring.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds one_mul, mul_one, natCast_zero, natCast_succ, intCast_ofNat, intCast_negSucc
Extends3
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances26
- SeparationQuotient
- Filter.Germ
- CStarMatrix
- TensorProduct
- Unitization
- WithConv
- Matrix
- HahnSeries
- LocallyConstant
- MeasureTheory.SimpleFunc
- MonoidAlgebra
- TrivSqZeroExt
- AddMonoidAlgebra
- DirectLimit
- SymAlg
- SkewMonoidAlgebra
- RingCon.Quotient
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
How is a type an instance?
Loading the hierarchy index…
Assumed by569
- Int.castRingHom
- RingHom.injective
- RingHom.range
- eq_intCast
- zsmul_eq_mul
- Int.cast_mul
- Subring.closure
- Subring.toSubsemiring
- map_intCast
- Subring.map
- Subring.op
- Subring.center
- Subring.unop
- Subring.comap
- Subring.subtype
- IsIdempotentElem.one_sub
- Subring.opEquiv
- Function.Periodic.int_mul
- Subring.subset_closure
- RingHom.map_sub
- MulRingSeminorm.toAddGroupSeminorm
- Subring.closure_le
- Subring.inclusion
- RingHom.rangeRestrict
- RingHom.eqLocus
- Subring.toAddSubgroup
- RingHom.injective_int
- Subring.prod
- RingHom.map_neg
- RingHom.mem_range
- MulRingNorm.toMulRingSeminorm
- mul_one_sub
- Ring.descPochhammer_eq_factorial_smul_choose
- mul_sub_one
- Subring.zero_mem
- Ring.choose_zero_right'
- Subring.mul_mem
- sub_one_mul
- Subring.copy
- Function.Periodic.sub_int_mul_eq
- Int.cast_commute
- intCast_mem
- mul_self_eq_one_iff
- Subring.gc_map_comap
- Function.Periodic.int_mul_sub_eq
- Subring.mk'
- Function.Periodic.sub_nat_mul_eq
- Function.Periodic.nat_mul_sub_eq
- CharZero.eq_neg_self_iff
- Subring.add_mem
Ancestors63
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommGroupWithOne
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddGroup
- AddGroupWithOne
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddMonoidWithOne
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Bracket
- 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
- NonAssocSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- Nonempty
- OfNat
- One
- SMul
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero