Theorems · Theorem · number theory
Nat.lt_ratSqrt_add_inv_prec_sq
∀ (x : ℕ) {prec : ℕ}, 0 < prec → ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2- Defined in
- Mathlib.Data.Rat.NatSqrt.Defs
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_zeroproof · cited by 1,870
- ne_of_gtproof · cited by 637
- add_mulproof · cited by 363
- pow_posproof · cited by 292
- mul_powproof · cited by 220
- Nat.cast_pos'proof · cited by 219
- div_mul_cancel₀proof · cited by 122
- Nat.ratSqrtstatement · cited by 7
- mul_lt_mul_iff_of_pos_rightproof · cited by 4
- Nat.lt_succ_sqrt'proof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- Nat.realSqrt_lt_ratSqrt_add_inv_precproof · cited by 0