Theorems · Theorem · number theory
Int.natCast_natAbs
∀ (n : ℤ), ↑n.natAbs = |n|
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- absstatement · cited by 1,814
- Int.abs_eq_natAbsproof · cited by 26
Cited by24
Results whose statement or proof uses this declaration.
- Nat.cast_natAbsproof · cited by 30
- NNRat.num_coeproof · cited by 14
- HasSum.nat_add_negproof · cited by 10
- Int.modEq_natAbsproof · cited by 5
- NumberField.absNorm_differentIdealproof · cited by 4
- NNReal.natCast_natAbsproof · cited by 3
- Rat.mulHeight₁_eq_maxproof · cited by 2
- AddCircle.ergodic_zsmulproof · cited by 2
- Nat.sq_add_sq_zmodEqproof · cited by 2
- HasProd.nat_mul_negproof · cited by 2
- fermatLastTheoremWith_nat_int_rat_tfaeproof · cited by 2
- Nat.exists_mem_span_nat_finset_of_geproof · cited by 1