isNat_realSqrt_of_isRat_negOfNat

Mathlib.Tactic.NormNum.RealSqrt

URI: https://scilib.ai/kg/mathlib#Tactic.NormNum.isNat_realSqrt_of_isRat_negOfNat

Lean4

theorem isNat_realSqrt_of_isRat_negOfNat {x : ℝ} {num : ℕ} {denom : ℕ} (h : IsRat x (.negOfNat num) denom) :
    IsNat √x (nat_lit 0) := by
  refine ⟨?_⟩
  obtain ⟨inv, rfl⟩ := h
  have h₁ : 0 ≤ (num : ℚ) * ⅟(denom : ℝ) := mul_nonneg (Nat.cast_nonneg' _) (invOf_nonneg.2 <| Nat.cast_nonneg' _)
  simpa [Nat.cast_zero, Real.sqrt_eq_zero', Int.cast_negOfNat, neg_mul, neg_nonpos] using h₁

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru