Mathlib Map

Theorems · Theorem · group theory

Units.isUnit

∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ), IsUnit ↑u
Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
116 results in Mathlib
Foundations
Depth 4 from the axioms, rests on 7 definitions · uses no axioms
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsUnit.map · cited by 104IsUnit.mapIsUnit.mk0 · cited by 33IsUnit.mk0Ring.inverse_unit · cited by 24Ring.inverse_unitInt.units_eq_one_or · cited by 20Int.units_eq_one_orIsUnit.neg · cited by 19IsUnit.negMulChar.one_apply_coe · cited by 13MulChar.one_apply_coenormalize_eq_one · cited by 10normalize_eq_oneCommute.isUnit_mul_iff · cited by 9Commute.isUnit_mul_iffPolynomial.eq_of_monic_of_associated · cited by 8Polynomial.eq_of_monic_of…NumberField.Units.norm · cited by 8Units.normZMod.isUnit_iff_coprime · cited by 7ZMod.isUnit_iff_coprimeisUnit_pow_iff · cited by 7isUnit_pow_iffIsUnit.inv · cited by 7IsUnit.invUnits.isOpen · cited by 6Units.isOpenIsLocalization.Away.of_associated · cited by 6Away.of_associatedMonoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valIsUnit · cited by 1602IsUnitUnits.isUnitCITED BYCITES

Cites4

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 · cited by 1,966
  • IsUnitstatement · cited by 1,602

Cited by117

Results whose statement or proof uses this declaration.