Polarization_apply — Mathlib

English

For any x in M, Polarization(x) equals the finite sum over i of coroot'_i(x) times coroot_i.

Русский

Для любого x в M поляризация применима как конечная сумма по i: Polarization(x) = ∑_i coroot'_i(x) · coroot_i.

LaTeX

$$$ P.Polarization(x) = \\sum_i P.coroot' i(x) \\cdot P.coroot i $$$

Lean4

@[simp]
theorem Polarization_apply (x : M) : P.Polarization x = ∑ i, P.coroot' i x • P.coroot i := by simp [Polarization]

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