reverse_apply — Mathlib

English

The reverse map is the identity on CliffordAlgebra Q.

Русский

Обратное отображение является тождественным на CliffordAlgebra(Q).

LaTeX

$$$\text{reverse}(x) = x\quad\forall x \in \operatorname{CliffordAlgebra}(Q)$$$

Lean4

/-- `reverse` is a no-op over `CliffordAlgebraComplex.Q`. -/
theorem reverse_apply (x : CliffordAlgebra Q) : x.reverse = x := by
  induction x using CliffordAlgebra.induction with
  | algebraMap r => exact reverse.commutes _
  | ι x => rw [reverse_ι]
  | mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]

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