Theorems · Inductive type · ring theory
NonUnitalNonAssocCommRing
Type u → Type u
A non-unital non-associative commutative ring is a NonUnitalNonAssocRing with commutative
multiplication.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by19
Results whose statement or proof uses this declaration.
- mul_self_eq_mul_self_iffstatement and proof · cited by 4
- NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing_injectivestatement and proof · cited by 1
- NonUnitalNonAssocCommRing.casesOnstatement and proof · cited by 1
- NonUnitalNonAssocCommRing.extstatement and proof · cited by 1
- NonUnitalNonAssocCommRing.mk.noConfusionstatement · cited by 0
- mul_self_sub_mul_selfstatement and proof · cited by 0
- two_nsmul_lie_lmul_lmul_add_add_eq_zerostatement and proof · cited by 0
- two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_addstatement and proof · cited by 0
- Function.Injective.nonAssocCommRingproof · cited by 0
- Function.Injective.nonUnitalCommRingproof · cited by 0
- Function.Injective.nonUnitalNonAssocCommRingstatement and proof · cited by 0
- Function.Surjective.nonUnitalCommRingproof · cited by 0