averageMap_invariant — Mathlib

English

For any v, the image averageMap(ρ) v lies in the invariants ρ.

Русский

Для любого v образ averageMap(ρ) v лежит в инвариантах ρ.

LaTeX

$$$$ averageMap\;\rho\; v \in \mathrm{invariants}\;\rho. $$$$

Lean4

/-- The `averageMap` sends elements of `V` to the subspace of invariants.
-/
theorem averageMap_invariant (v : V) : averageMap ρ v ∈ invariants ρ := fun g => by
  rw [averageMap, ← asAlgebraHom_single_one, ← Module.End.mul_apply, ← map_mul (asAlgebraHom ρ), mul_average_left]

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