changeForm_one

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

URI: https://scilib.ai/kg/mathlib#CliffordAlgebra.changeForm_one

English

The change of form map fixes scalars: applying changeForm to the scalar 1 yields 1.

Русский

Изменение формы фиксирует скаляры: применение changeForm к скаляру 1 даёт 1.

LaTeX

$$$ \text{changeForm}(h)(1) = 1 $$$

Lean4

@[simp]
theorem changeForm_one : changeForm h (1 : CliffordAlgebra Q) = 1 := by simpa using changeForm_algebraMap h (1 : R)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru