self_comp_coPolarization_eq_corootForm

English

The self-composition of the forward map with CoPolarization equals CorootForm: P.toLinearMap ∘ P.CoPolarization = P.CorootForm.

Русский

Самокомпозиция прямого отображения с Copolarization дает CorootForm: P.toLinearMap ∘ P.CoPolarization = P.CorootForm.

LaTeX

$$$ P.toLinearMap \\circ P.CoPolarization = P.CorootForm $$$

Lean4

theorem self_comp_coPolarization_eq_corootForm : P.toLinearMap ∘ₗ P.CoPolarization = P.CorootForm :=
  P.flip.flip_comp_polarization_eq_rootForm

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