changeForm_algebraMap — Mathlib

English

The change of form map respects algebra scalars: applying changeForm to the image of an element r ∈ R under algebraMap is the same as algebraMap of r into the target Clifford algebra.

Русский

Изменение формы сохраняет скаляры: применяя changeForm к образу скаляра r через algebraMap, получаем тот же результат, что и algebraMap в целевой алгебре Клиффорда.

LaTeX

$$$ \text{changeForm}(h)(\text{algebraMap}_R( r )) = \text{algebraMap}_R( r ) $$$

Lean4

@[simp]
theorem changeForm_algebraMap (r : R) : changeForm h (algebraMap R _ r) = algebraMap R _ r :=
  (foldr_algebraMap _ _ _ _ _).trans <| Eq.symm <| Algebra.algebraMap_eq_smul_one r

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