toLinearMap_apply_PolarizationIn — Mathlib

English

The linear map toLinearMap applied to y, after PolarizationIn on x, yields RootForm via algebra map.

Русский

Линейное отображение toLinearMap, применяемое к y после PolarizationIn на x, даёт RootForm через алгебраическое отображение.

LaTeX

$$$P.toLinearMap\\ y\\ (P.PolarizationIn S x) = (\\mathrm{algebraMap}\ S R)(P.RootFormIn S x y)$$$

Lean4

theorem toLinearMap_apply_PolarizationIn (x y : P.rootSpan S) :
    P.toLinearMap y (P.PolarizationIn S x) = (algebraMap S R) (P.RootFormIn S x y) :=
  by
  rw [PolarizationIn_eq, algebraMap_rootFormIn]
  exact toLinearMap_apply_apply_Polarization P x y

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