changeForm_ι_mul — Mathlib

English

The change of form maps the product ι_Q(m) * x to ι_Q'(m) * changeForm(h) x minus the contraction by B evaluated at m acting on changeForm(h) x.

Русский

Изменение формы переводит произведение ι_Q(m) на ι_Q'(m) * changeForm(h) x минус конракция по B при m, действующая на changeForm(h) x.

LaTeX

$$$ changeForm(h)(\iota_Q(m) * x) = \iota_{Q'}(m) * changeForm(h) x - B(m, \cdot) ⌟ changeForm(h) x $$$

Lean4

theorem changeForm_ι_mul (m : M) (x : CliffordAlgebra Q) :
    changeForm h (ι Q m * x) = ι Q' m * changeForm h x - B m⌋changeForm h x :=
  (foldr_mul _ _ _ _ _ _).trans <| by rw [foldr_ι]; rfl

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