involute_eq_of_mem_even — Mathlib

English

Let Q be a quadratic form on M and x ∈ Clifford(Q) with x ∈ evenOdd(Q, 0). Then involute(x) = x; i.e., the involute fixes even elements.

Русский

Пусть Q — квадратичная форма на M, и x ∈ Clifford(Q) принадлежит evenOdd(Q,0). Тогда involute(x) = x; то есть involute фиксирует элементы четной части.

LaTeX

$$$ x \\in \\mathrm{evenOdd}(Q,0) \\Rightarrow \\mathrm{involute}(x) = x $$$

Lean4

theorem involute_eq_of_mem_even {x : CliffordAlgebra Q} (h : x ∈ evenOdd Q 0) : involute x = x := by
  induction x, h using even_induction with
  | algebraMap r => exact AlgHom.commutes _ _
  | add x y _hx _hy ihx ihy => rw [map_add, ihx, ihy]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx => rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg]

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