sqrt_eq

Mathlib.Data.Rat.Sqrt

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

English

For any rational q, sqrt(q^2) = |q|.

Русский

Для любого рационального q верно sqrt(q^2) = |q|.

LaTeX

$$$ \operatorname{sqrt}(q^2) = |q| $$$

Lean4

theorem sqrt_eq (q : ℚ) : Rat.sqrt (q * q) = |q| := by
  rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]

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

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

Разделы

Аффилиация

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