isNat_realSqrt_neg

Mathlib.Tactic.NormNum.RealSqrt

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

Lean4

theorem isNat_realSqrt_neg {x : ℝ} {nx : ℕ} (h : IsInt x (Int.negOfNat nx)) : IsNat √x (nat_lit 0) :=
  ⟨by simp [Real.sqrt_eq_zero', h.out]⟩

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

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

Разделы

Аффилиация

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