Mathlib Map

Theorems · Theorem · number theory

Int.isUnit_iff_natAbs_eq

∀ {u : ℤ}, IsUnit u ↔ u.natAbs = 1
Defined in
Mathlib.Algebra.Group.Int.Units
Cited by
6 results in Mathlib
Foundations
Depth 40 from the axioms · uses propext, Classical.choice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Nat.prime_iff_prime_int · cited by 27Nat.prime_iff_prime_intnorm_isUnit_zsmul · cited by 3norm_isUnit_zsmulInt.isUnit_iff_abs_eq · cited by 1Int.isUnit_iff_abs_eqnorm_zpow_isUnit · cited by 1norm_zpow_isUnitInt.IsUnit.natAbs_eq · cited by 0IsUnit.natAbs_eqZsqrtd.isUnit_iff_norm_isUnit · cited by 0Zsqrtd.isUnit_iff_norm_is…IsUnit · cited by 1602IsUnitInt.isUnit_iff_natAbs_eqCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • IsUnitstatement · cited by 1,602

Cited by6

Results whose statement or proof uses this declaration.