sum_polar_sub_repr_sq — Mathlib

English

For a quadratic map Q, a basis bm of M, and x ∈ M, the coordinate expression difference between polar contributions and the coordinate quadratic form equals Q(x).

Русский

Для квадратичного отображения Q, базиса bm множества M и вектора x∈M разность координатного выражения поляризационных членов и координатной квадратичной формы равна Q(x).

LaTeX

$$linearCombination R (polarSym2 Q ∘ Sym2.map bm) (bm.repr x).sym2Mul - linearCombination R (Q ∘ bm) (bm.repr x * bm.repr x) = Q x$$

Lean4

theorem sum_polar_sub_repr_sq (Q : QuadraticMap R M N) (bm : Basis ι R M) (x : M) :
    linearCombination R (polarSym2 Q ∘ Sym2.map bm) (bm.repr x).sym2Mul -
        linearCombination R (Q ∘ bm) (bm.repr x * bm.repr x) =
      Q x :=
  by rw [← apply_linearCombination', Basis.linearCombination_repr]

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