map_one

Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

URI: https://scilib.ai/kg/mathlib#CliffordAlgebra.reverse.map_one

English

In the Clifford algebra Cl(Q), the reverse map fixes the multiplicative identity: reverse(1) = 1.

Русский

В клиффордовой алгебре Cl(Q) обратное сохраняет единицу: reverse(1) = 1.

LaTeX

$$$ reverse(1) = 1 $$$

Lean4

@[simp]
protected theorem map_one : reverse (1 : CliffordAlgebra Q) = 1 :=
  op_injective (map_one reverseOp)

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

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

Разделы

Аффилиация

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