PolarizationIn_eq — Mathlib

English

The co-polarization In map coincides with the CoPolarization map when restricted appropriately.

Русский

Ко-поляризация In совпадает с CoPolarization при соответствующем ограничении.

LaTeX

$$$P.CoPolarizationIn\\ S x = P.CoPolarization x$$$

Lean4

theorem PolarizationIn_eq (x : P.rootSpan S) : P.PolarizationIn S x = P.Polarization x :=
  by
  simp only [PolarizationIn, LinearMap.coeFn_sum, LinearMap.coe_comp, Finset.sum_apply, comp_apply,
    LinearMap.toSpanSingleton_apply, Polarization_apply]
  refine Finset.sum_congr rfl fun i hi ↦ ?_
  rw [algebra_compatible_smul R (P.coroot'In S i x) (P.coroot i), algebraMap_coroot'In_apply]

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