Theorems · Theorem · number theory
Int.natAbs_of_isUnit
∀ {u : ℤ}, IsUnit u → u.natAbs = 1- Defined in
- Mathlib.Algebra.Group.Int.Units
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 36 from the axioms · uses propext, Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsUnitstatement and proof · cited by 1,602
- IsUnit.unitproof · cited by 252
- Int.units_natAbsproof · cited by 3
Cited by11
Results whose statement or proof uses this declaration.
- preNormEDS_oneproof · cited by 8
- Polynomial.Chebyshev.degree_Tproof · cited by 7
- Int.isUnit_eq_one_orproof · cited by 6
- Polynomial.Chebyshev.degree_U_of_ne_neg_oneproof · cited by 2
- PythagoreanTriple.classifiedproof · cited by 1
- IsCyclotomicExtension.Rat.discrproof · cited by 1
- Archimedean.ratLt_nonemptyproof · cited by 1
- Polynomial.Chebyshev.leadingCoeff_Tproof · cited by 1
- padicValInt.oneproof · cited by 1
- Archimedean.embedRealFun_strictMonoproof · cited by 1
- complEDS_oneproof · cited by 1