Mathlib Map

Theorems · Theorem · group theory

IsUnit.eq_one

∀ {M : Type u_1} [inst : Monoid M] {a : M} [Subsingleton Mˣ], IsUnit a → a = 1
Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
1 results in Mathlib
Foundations
Depth 9 from the axioms · uses propext
Assumes
MonoidSubsingleton
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

isUnit_iff_eq_one · cited by 4isUnit_iff_eq_oneMonoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valIsUnit · cited by 1602IsUnitUnits.eq_one · cited by 3Units.eq_oneIsUnit.eq_oneCITED BYCITES

Cites5

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
  • Unitsstatement and proof · cited by 2,804
  • Units.valproof · cited by 1,966
  • IsUnitstatement and proof · cited by 1,602
  • Units.eq_oneproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.