CoPolarization_apply — Mathlib

English

CoPolarization is the invariant linear map from coweight space N to weight space M, defined as CoPolarization = P.flip.Polarization.

Русский

Кополяризация — это инвариантное линейное отображение из косвой весовой пространства N в пространство весов M, задаваемое как Copolarization = P.flip.Polarization.

LaTeX

$$$ P.CoPolarization = P.flip.Polarization $$$

Lean4

@[simp]
theorem CoPolarization_apply (x : N) : P.CoPolarization x = ∑ i, P.root' i x • P.root i :=
  P.flip.Polarization_apply x

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