equiv_symm_eps

Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

URI: https://scilib.ai/kg/mathlib#CliffordAlgebraDualNumber.equiv_symm_eps

English

The inverse equivalence sends ε back to ι(0) 1 in the Clifford algebra.

Русский

Обратное эквивалентности возвращает ε к ι(0) 1 в клиффордовой алгебре.

LaTeX

$$equiv.symm(ε) = ι_{0}(1)$$

Lean4

@[simp]
theorem equiv_symm_eps : CliffordAlgebraDualNumber.equiv.symm (eps : R[ε]) = ι (0 : QuadraticForm R R) 1 :=
  DualNumber.lift_apply_eps _

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

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

Разделы

Аффилиация

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