charAlgHom_apply — Mathlib

English

The evaluation formula shows how AddMonoidAlgebra coefficients combine with character evaluations to yield values of the algebra hom.

Русский

Формула вычисления демонстрирует, как коэффициенты из AddMonoidAlgebra сочетаются с оценками характерной функции, чтобы получить значения алгебра-гомоморфизма.

LaTeX

$$$\\text{charAlgHom}(he,hL)(w)(v) = \\sum_{a \\in w.support} w(a) \\; e(L(v,a)).$$$

Lean4

@[simp]
theorem charAlgHom_apply (w : AddMonoidAlgebra ℂ W) (v : V) :
    charAlgHom he hL w v = ∑ a ∈ w.support, w a * (e (L v a) : ℂ) :=
  by
  simp only [charAlgHom, AddMonoidAlgebra.lift_apply]
  rw [Finsupp.sum_of_support_subset w subset_rfl]
  · simp only [coe_sum, coe_smul, charMonoidHom_apply, smul_eq_mul, Finset.sum_apply]
    rfl
  · simp

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