isNat_nnrealSqrt

Mathlib.Tactic.NormNum.RealSqrt

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

Lean4

theorem isNat_nnrealSqrt {x : ℝ≥0} {nx ny : ℕ} (h : IsNat x nx) (hy : ny * ny = nx) : IsNat (NNReal.sqrt x) ny :=
  ⟨by simp [h.out, ← hy]⟩

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

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

Разделы

Аффилиация

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