Theorems · Theorem · group theory
AddMonoid.ext
∀ {M : Type u} ⦃m₁ m₂ : AddMonoid M⦄, HAdd.hAdd = HAdd.hAdd → m₁ = m₂- Defined in
- Mathlib.Algebra.Group.Ext
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidHomproof · cited by 3,230
- AddMonoidstatement and proof · cited by 2,864
- AddZeroClassproof · cited by 1,237
- AddMonoid.toZeroproof · cited by 325
- AddSemigroupproof · cited by 136
- AddMonoidHom.map_nsmulproof · cited by 18
- NSMul.nsmulproof · cited by 8
- AddMonoid.casesOnproof · cited by 4
- NSMulproof · cited by 4
- AddZeroClass.extproof · cited by 2
- NSMul.casesOnproof · cited by 1
- AddSemigroup.casesOnproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- AddGroup.extproof · cited by 4
- AddCommMonoid.extproof · cited by 4
- AddMonoidWithOne.extproof · cited by 3
- AddLeftCancelMonoid.extproof · cited by 2
- SubNegMonoid.extproof · cited by 2
- AddRightCancelMonoid.extproof · cited by 1
- AddMonoid.ext_iffproof · cited by 0