char_mem_charPoly — Mathlib

English

The lemma asserts that each basic char function is contained in the charPoly subalgebra.

Русский

Лемма утверждает, что каждая базовая функция-символ содержится в подалгебре CharPoly.

LaTeX

$$$\\text{char}(he,hL,w) \\in \\text{charPoly}(he,hL)\\quad\\text{for all } w \\in W.$$$

Lean4

theorem char_mem_charPoly (w : W) : char he hL w ∈ charPoly he hL :=
  by
  rw [mem_charPoly]
  refine ⟨AddMonoidAlgebra.single w 1, ?_⟩
  ext v
  simp only [char_apply, AddMonoidAlgebra.single]
  rw [Finset.sum_eq_single w]
  · simp only [Finsupp.single_eq_same, one_mul]
  · simp [Finsupp.single_apply_ne_zero]
  · simp

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