Theorems · Theorem · number theory
Int.abs_eq_natAbs
∀ (a : ℤ), |a| = ↑a.natAbs
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 34 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- absstatement and proof · cited by 1,814
- le_of_ltproof · cited by 1,175
- abs_of_nonnegproof · cited by 279
- abs_of_nonposproof · cited by 53
Cited by26
Results whose statement or proof uses this declaration.
- Int.natCast_natAbsproof · cited by 24
- Int.eq_zero_of_abs_lt_dvdproof · cited by 3
- norm_natAbs_smulproof · cited by 2
- AddCircle.ergodic_zsmulproof · cited by 2
- norm_pow_natAbsproof · cited by 2
- Rat.abs_def'statement and proof · cited by 2
- AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_divproof · cited by 2
- Int.ediv_eq_zero_of_lt_absproof · cited by 1
- Int.natAbs_lt_iff_mul_self_ltproof · cited by 1
- Int.natAbs_le_iff_mul_self_leproof · cited by 1
- Int.abs_negOnePowproof · cited by 1
- Int.isUnit_iff_abs_eqproof · cited by 1