evenOdd_comap_involute — Mathlib

English

The comap of evenOdd Q n under involute equals evenOdd Q n.

Русский

Сопряжение подмодуля evenOdd Q n через involute дает тот же подмодуль.

LaTeX

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

Lean4

@[simp]
theorem evenOdd_comap_involute (n : ZMod 2) :
    (evenOdd Q n).comap (involute : CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q).toLinearMap = evenOdd Q n := by
  rw [← submodule_map_involute_eq_comap, evenOdd_map_involute]

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