isNat_realSqrt

Mathlib.Tactic.NormNum.RealSqrt

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

Lean4

theorem isNat_realSqrt {x : ℝ} {nx ny : ℕ} (h : IsNat x nx) (hy : ny * ny = nx) : IsNat (√x) ny :=
  ⟨by simp [h.out, ← hy]⟩

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

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

Разделы

Аффилиация

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