changeForm_self — Mathlib

English

The changeForm with zero_proof equals the identity map on CliffordAlgebra Q.

Русский

Изменение формы с нулевым доказательством равно тождестенной карте на CliffordAlgebra(Q).

LaTeX

$$$ \text{changeForm}(\text{zero_proof}) = \mathrm{Id}_{\mathrm{CliffordAlgebra}(Q)} $$$

Lean4

@[simp]
theorem changeForm_self : changeForm changeForm.zero_proof = (LinearMap.id : CliffordAlgebra Q →ₗ[R] _) :=
  LinearMap.ext <| changeForm_self_apply

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