Mathlib Map

Theorems · Theorem · group theory

Units.ext_iff

∀ {α : Type u} [inst : Monoid α] {u v : αˣ}, u = v ↔ ↑u = ↑v
Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
29 results in Mathlib
Foundations
Depth 12 from the axioms · uses no axioms
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ZMod.val_coe_unit_coprime · cited by 6ZMod.val_coe_unit_coprimeInt.units_sq · cited by 5Int.units_sqPowerSeries.IsWeierstrassFactorization.elim · cited by 5IsWeierstrassFactorizatio…Int.units_natAbs · cited by 3Int.units_natAbsmodularCyclotomicCharacter.toFun_spec · cited by 3modularCyclotomicCharacte…rootsOfUnity.integer_power_of_ringEquiv · cited by 2rootsOfUnity.integer_powe…ZMod.wilsons_lemma · cited by 2ZMod.wilsons_lemmaIdeal.rootsOfUnityMapQuot_injective · cited by 2Ideal.rootsOfUnityMapQuot…ValuativeRel.subsingleton_units_valueGroupWithZero_of_trivialRel · cited by 2ValuativeRel.subsingleton…modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow · cited by 2modularCyclotomicCharacte…MulChar.apply_mem_algebraAdjoin_of_pow_eq_one · cited by 2MulChar.apply_mem_algebra…MvPowerSeries.invOfUnit_eq' · cited by 1MvPowerSeries.invOfUnit_e…Complex.mem_rootsOfUnity · cited by 1Complex.mem_rootsOfUnityDirichletCharacter.factorsThrough_gcd · cited by 1DirichletCharacter.factor…MulChar.exists_apply_ne_one_iff_exists_monoidHom · cited by 1MulChar.exists_apply_ne_o…Monoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valUnits.ext · cited by 86Units.extUnits.ext_iffCITED 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 and proof · cited by 1,966
  • Units.extproof · cited by 86

Cited by29

Results whose statement or proof uses this declaration.