changeForm_self_apply — Mathlib

English

For any x in CliffordAlgebra Q, applying changeForm with zero_proof to x yields x themselves (self-application).

Русский

Для любого x ∈ CliffordAlgebra(Q) применение changeForm с нулевым доказательством к x даёт сам x.

LaTeX

$$$ changeForm(h)(x) = x \quad \text{for all } x \in CliffordAlgebra(Q)$$$

Lean4

theorem changeForm_self_apply (x : CliffordAlgebra Q) : changeForm (Q' := Q) changeForm.zero_proof x = x := by
  induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [changeForm_algebraMap]
  | add _ _ hx hy => rw [map_add, hx, hy]
  | ι_mul _ _ hx => rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply, sub_zero]

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