sqrt_natCast

Mathlib.Data.Rat.Sqrt

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

← MathLib Explorer

English

For any natural n, Rat.sqrt(n : ℚ) = Nat.sqrt(n).

Русский

Для любого натурального n выполняется Rat.sqrt(n : ℚ) = Nat.sqrt(n).

LaTeX

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

Lean4

@[simp, norm_cast]
theorem sqrt_natCast (n : ℕ) : Rat.sqrt (n : ℚ) = Nat.sqrt n := by
  rw [← Int.cast_natCast, sqrt_intCast, Int.sqrt_natCast, Int.cast_natCast]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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