averageMap_id — Mathlib

English

On invariants, the averaging map acts as the identity.

Русский

На инвариантах среднее отображение равно тождественному отображению.

LaTeX

$$$$ averageMap\;\rho\; v = v \quad \text{if } v \in \mathrm{invariants}\;\rho. $$$$

Lean4

/-- The `averageMap` acts as the identity on the subspace of invariants.
-/
theorem averageMap_id (v : V) (hv : v ∈ invariants ρ) : averageMap ρ v = v :=
  by
  rw [mem_invariants] at hv
  simp [average, map_sum, hv, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k _ v, smul_smul]

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