normSq_eq_norm_mul_self

Mathlib.Analysis.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.normSq_eq_norm_mul_self

English

For every quaternion a ∈ ℍ, the squared norm equals the product of the norm with itself: ||a||^2 = ||a|| · ||a||.

Русский

Для любого кватерниона a ∈ ℍ верно: ||a||^2 = ||a|| · ||a||.

LaTeX

$$$\\|a\\|^2 = \\|a\\| \\cdot \\|a\\| \\quad (a \\in \\mathbb{H}).$$$

Lean4

theorem normSq_eq_norm_mul_self (a : ℍ) : normSq a = ‖a‖ * ‖a‖ := by rw [← inner_self, real_inner_self_eq_norm_mul_norm]

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

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

Разделы

Аффилиация

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