flip_comp_polarization_eq_rootForm

English

The composition of the flipped map with Polarization equals RootForm: P.flip ∘ P.Polarization = P.RootForm.

Русский

Состав перевернутого отображения с Polarization равен RootForm: P.flip ∘ P.Polarization = P.RootForm.

LaTeX

$$$ P.flip \\circ P.Polarization = P.RootForm $$$

Lean4

theorem flip_comp_polarization_eq_rootForm : P.flip.toLinearMap ∘ₗ P.Polarization = P.RootForm := by ext;
  simp [rootForm_apply_apply, RootPairing.flip]

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