normSq_ofReal

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.normSq_ofReal

English

As above, the norm-squared of a real number equals its square.

Русский

Как и ранее, норма в квадрате вещественного числа равна его квадрату.

LaTeX

$$$\operatorname{normSq}(r) = r^2$$$

Lean4

@[simp]
theorem normSq_ofReal (r : ℝ) : normSq r = r * r := by simp [normSq, ofReal]

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

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

Разделы

Аффилиация

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