lift_ι — Mathlib

English

The EquivEven Q induces a Q'-map from M×R to the Clifford algebra, matching expanded quadratic form.

Русский

Эквивиалентность EquivEven Q задаёт отображение Q' на M×R в CliffordAlgebra, совпадающее с расширенной квадратичной формой.

LaTeX

$$Q' Q : QuadraticForm R (M×R) := Q.prod (-QuadraticMap.sq)$$

Lean4

@[simp]
theorem lift_ι (f : EvenHom Q A) (m₁ m₂ : M) : even.lift Q f ((even.ι Q).bilin m₁ m₂) = f.bilin m₁ m₂ :=
  even.lift.aux_ι _ _ _

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