sumOfConjugates_apply — Mathlib

English

For any v ∈ W, the value of the sum of conjugates applied to v equals the finite sum over G of the conjugates applied to v.

Русский

Для любого v ∈ W значение суммы конъюгатов на v равно конечной сумме по g ∈ G от π^g(v).

LaTeX

$$$\forall v \in W,\; π.sumOfConjugates G v = \sum_{g\in G} π.conjugate g v$$$

Lean4

theorem sumOfConjugates_apply (v : W) : π.sumOfConjugates G v = ∑ g : G, π.conjugate g v :=
  LinearMap.sum_apply _ _ _

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