involute_mem_evenOdd_iff — Mathlib

English

Let Q be a quadratic form on M and let x be an element of the Clifford algebra Clifford(Q). For any n ∈ Z/2Z, the involute map preserves membership in the even-odd subspace: involute(x) ∈ evenOdd(Q, n) iff x ∈ evenOdd(Q, n).

Русский

Пусть Q — квадратичная форма на M, и пусть x — элемент клиффордовой алгебры Clifford(Q). Для любого n ∈ Z/2Z отображение involute сохраняет принадлежность к подпространству четности: involute(x) ∈ evenOdd(Q, n) тогда и только тогда, когда x ∈ evenOdd(Q, n).

LaTeX

$$$\\text{involute}(x) \\in \\mathrm{evenOdd}(Q,n) \\iff x \\in \\mathrm{evenOdd}(Q,n)$$$

Lean4

@[simp]
theorem involute_mem_evenOdd_iff {x : CliffordAlgebra Q} {n : ZMod 2} : involute x ∈ evenOdd Q n ↔ x ∈ evenOdd Q n :=
  SetLike.ext_iff.mp (evenOdd_comap_involute Q n) x

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