reverse_comp_involute — Mathlib

English

Reverse and involute commute as linear maps: reverse ∘ involute = involute ∘ reverse.

Русский

Reverse и involute коммутируют как линейные отображения: reverse ∘ involute = involute ∘ reverse.

LaTeX

$$$ reverse \circ involute = involute \circ reverse $$$

Lean4

theorem reverse_comp_involute :
    reverse.comp involute.toLinearMap = (involute.toLinearMap.comp reverse : _ →ₗ[R] CliffordAlgebra Q) :=
  by
  ext x
  simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply]
  induction x using CliffordAlgebra.induction with
  | algebraMap => simp
  | ι => simp
  | mul a b ha hb => simp only [ha, hb, reverse.map_mul, map_mul]
  | add a b ha hb => simp only [ha, hb, reverse.map_add, map_add]

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