CoPolarizationIn — Mathlib

English

CoPolarizationIn is the restriction of PolarizationIn to the coroot span, given by flipping polarization.

Русский

CoPolarizationIn — это ограничение PolarizationIn на коротрspan, получаемое разворотом поляризации.

LaTeX

$$$\\text{CoPolarizationIn} : P.corootSpan S \\to_l[S] M = P.flip.PolarizationIn S$$$

Lean4

/-- Polarization restricted to `S`-span of roots. -/
def CoPolarizationIn : P.corootSpan S →ₗ[S] M :=
  P.flip.PolarizationIn S

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