Theorems · Theorem · order theory
Nat.abs_cast
∀ {R : Type u_1} [inst : Ring R] [inst_1 : Lattice R] [IsOrderedRing R] (n : ℕ), |↑n| = ↑n- Defined in
- Mathlib.Data.Nat.Cast.Order.Ring
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RingLatticeIsOrderedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- absstatement · cited by 1,814
- Latticestatement and proof · cited by 916
- IsOrderedRingstatement and proof · cited by 777
- abs_of_nonnegproof · cited by 279
- Nat.cast_nonnegproof · cited by 109
Cited by36
Results whose statement or proof uses this declaration.
- Nat.abs_ofNatproof · cited by 12
- summable_pow_mul_jacobiTheta₂_term_boundproof · cited by 6
- HurwitzKernelBounds.summable_f_natproof · cited by 5
- hasSum_choose_mul_geometric_of_norm_lt_one'proof · cited by 4
- HurwitzZeta.hasSum_nat_cosZetaproof · cited by 4
- Pell.exists_of_not_isSquareproof · cited by 3
- HurwitzZeta.hasSum_nat_sinZetaproof · cited by 3
- summable_norm_mul_geometric_of_norm_lt_oneproof · cited by 2
- Behrend.norm_of_mem_sphereproof · cited by 2
- norm_natCast_eq_mul_norm_oneproof · cited by 2
- Rat.mulHeight₁_eq_maxproof · cited by 2
- HurwitzZeta.hasSum_int_completedSinZetaproof · cited by 2