reverseOp_ι

Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

URI: https://scilib.ai/kg/mathlib#CliffordAlgebra.reverseOp_ι

English

Applying reverseOp to a generator yields the opposite generator: reverseOp(ι_Q(m)) = op(ι_Q(m)).

Русский

Применение reverseOp к генератору даёт opp-генератор: reverseOp(ι_Q(m)) = op(ι_Q(m)).

LaTeX

$$$ \mathrm{reverseOp}(\iota_Q(m)) = \mathrm{op}(\iota_Q(m)). $$$

Lean4

@[simp]
theorem reverseOp_ι (m : M) : reverseOp (ι Q m) = op (ι Q m) :=
  lift_ι_apply _ _ _

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

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

Разделы

Аффилиация

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