sumOfConjugates — Mathlib

English

Given a finite group G and a linear map π: W → V, form the sum of its g-conjugates over all g ∈ G. This yields a new k-linear map W → V, namely sum_{g∈G} π^g.

Русский

Для конечной группы G и линейного отображения π: W → V образуется сумма всех конъюгатов π^g по g ∈ G, которая задаёт новое линейное отображение W → V: ∑_{g∈G} π^g.

LaTeX

$$$\operatorname{sumOfConjugates} : W \to V := \sum_{g\in G} π.conjugate g$$$

Lean4

/-- The sum of the conjugates of `π` by each element `g : G`, as a `k`-linear map.

(We postpone dividing by the size of the group as long as possible.)
-/
def sumOfConjugates : W →ₗ[k] V :=
  ∑ g : G, π.conjugate g

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