Mathlib Map

Theorems · Theorem · group theory

IsUnit.unit_of_val_units

∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ} (h : IsUnit ↑a), h.unit = a
Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
5 results in Mathlib
Foundations
Depth 12 from the axioms · uses Classical.choice
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Ring.inverse_unit · cited by 24Ring.inverse_unitMulChar.ofUnitHom_coe · cited by 1MulChar.ofUnitHom_coePi.quasispectrum_eq · cited by 1Pi.quasispectrum_eqProd.quasispectrum_eq · cited by 1Prod.quasispectrum_eqquasispectrum.mem_of_not_quasiregular · cited by 0quasispectrum.mem_of_not_…Monoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valIsUnit · cited by 1602IsUnitIsUnit.unit · cited by 252IsUnit.unitUnits.ext · cited by 86Units.extIsUnit.unit_of_val_unitsCITED BYCITES

Cites6

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.valstatement and proof · cited by 1,966
  • IsUnitstatement and proof · cited by 1,602
  • IsUnit.unitstatement · cited by 252
  • Units.extproof · cited by 86

Cited by5

Results whose statement or proof uses this declaration.