Theorems · Theorem · group theory
Monoid.ext
∀ {M : Type u} ⦃m₁ m₂ : Monoid M⦄, HMul.hMul = HMul.hMul → 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.
- Monoidstatement and proof · cited by 3,887
- MonoidHomproof · cited by 3,629
- MulOneClassproof · cited by 1,018
- Semigroupproof · cited by 202
- Monoid.toOneproof · cited by 34
- MonoidHom.map_powproof · cited by 30
- NPowproof · cited by 5
- Monoid.casesOnproof · cited by 4
- MulOneClass.extproof · cited by 3
- NPow.npowproof · cited by 3
- NPow.casesOnproof · cited by 1
- Semigroup.casesOnproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- Semiring.extproof · cited by 5
- Group.extproof · cited by 3
- CommMonoid.extproof · cited by 2
- DivInvMonoid.extproof · cited by 2
- LeftCancelMonoid.extproof · cited by 2
- RightCancelMonoid.extproof · cited by 1
- Monoid.ext_iffproof · cited by 0