reverse_mem_evenOdd_iff — Mathlib

English

Let Q be a quadratic form on M and n ∈ Z/2Z. If x ∈ Clifford(Q) then reverse(x) ∈ evenOdd(Q, n) iff x ∈ evenOdd(Q, n); i.e., the reverse operation preserves the even-odd subspaces.

Русский

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

LaTeX

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

Lean4

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

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