sqrt_natCast

Mathlib.Data.Int.Sqrt

URI: https://scilib.ai/kg/mathlib#Int.sqrt_natCast

English

For every natural n, Int.sqrt(n) equals Nat.sqrt(n) after identifying Nat.sqrt(n) with an integer.

Русский

Для каждого натурального n: Int.sqrt(κ(n)) = Nat.sqrt(n), где Nat.sqrt(n) приводится к целому.

LaTeX

$$$\mathrm{Int.sqrt} (n) = \mathrm{Nat.sqrt}\, n$ (как целое число)$$

Lean4

@[simp, norm_cast]
theorem sqrt_natCast (n : ℕ) : Int.sqrt (n : ℤ) = Nat.sqrt n := by rw [sqrt, toNat_natCast]

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

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

Разделы

Аффилиация

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