sqrt_ofNat

Mathlib.Data.Rat.Sqrt

URI: https://scilib.ai/kg/mathlib#Rat.sqrt_ofNat

English

For every natural n, Rat.sqrt(ofNat(n)) = Nat.sqrt(OfNat.ofNat n).

Русский

Для каждого натурального n верно Rat.sqrt(ofNat(n)) = Nat.sqrt(OfNat.ofNat n).

LaTeX

$$$ \operatorname{Rat.sqrt}(\operatorname{ofNat}(n)) = \operatorname{Nat.sqrt}(\operatorname{OfNat.ofNat}(n)) $$$

Lean4

@[simp]
theorem sqrt_ofNat (n : ℕ) : Rat.sqrt (ofNat(n) : ℚ) = Nat.sqrt (OfNat.ofNat n) :=
  sqrt_natCast _

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

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

Разделы

Аффилиация

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