normSq_star

Mathlib.Algebra.Quaternion

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

English

normSq is invariant under star: normSq (star a) = normSq a.

Русский

normSq сохраняется после сопряжения: normSq (star a) = normSq a.

LaTeX

$$$ normSq (star a) = normSq a $$$

Lean4

@[simp]
theorem normSq_star : normSq (star a) = normSq a := by simp [normSq_def']

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

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

Разделы

Аффилиация

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