involute_comp_involute

Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

URI: https://scilib.ai/kg/mathlib#CliffordAlgebra.involute_comp_involute

English

Involuting twice gives the identity on CliffordAlgebra Q: involute ∘ involute = id.

Русский

Двойное применение инволюции даёт тождественное отображение: involute ∘ involute = id.

LaTeX

$$$ \text{involute} \circ \text{involute} = \mathrm{id}_{\mathrm{CliffordAlgebra}(Q)}. $$$

Lean4

@[simp]
theorem involute_comp_involute : involute.comp involute = AlgHom.id R (CliffordAlgebra Q) := by ext; simp

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

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

Разделы

Аффилиация

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