evenOdd_map_involute — Mathlib

English

For any parity n in Z/2Z, the involute preserves the evenOdd submodule: (evenOdd Q n).map involute = evenOdd Q n.

Русский

Для любого паритета n в Z/2Z инфлуента сохраняет подмодуль evenOdd: (evenOdd Q n).map involute = evenOdd Q n.

LaTeX

$$$ (evenOdd Q n).map (involute.toLinearMap) = evenOdd Q n $$$

Lean4

@[simp]
theorem evenOdd_map_involute (n : ZMod 2) :
    (evenOdd Q n).map (involute : CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q).toLinearMap = evenOdd Q n := by
  simp_rw [evenOdd, Submodule.map_iSup, Submodule.map_pow, ι_range_map_involute]

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