involute_eq_of_mem_odd — Mathlib

English

Let Q be a quadratic form on M and x ∈ Clifford(Q) with x ∈ evenOdd(Q, 1). Then involute(x) = -x; i.e., involute acts as negation on odd elements.

Русский

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

LaTeX

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

Lean4

theorem involute_eq_of_mem_odd {x : CliffordAlgebra Q} (h : x ∈ evenOdd Q 1) : involute x = -x := by
  induction x, h using odd_induction with
  | ι m => exact involute_ι _
  | add x y _hx _hy ihx ihy => rw [map_add, ihx, ihy, neg_add]
  | ι_mul_ι_mul m₁ m₂ x _hx ihx => rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]

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