toWeightBasis_repr_root — Mathlib

English

The weight basis repr of coroot i yields a unit vector at i; i.e., the representation corresponds to the single unit support at i.

Русский

Представление в весовом базисе ко-роот i даёт единичный вектор на i.

LaTeX

$$b.toWeightBasis.repr (P.coroot i) = Finsupp.single i 1$$

Lean4

@[simp]
theorem toWeightBasis_repr_root (i : b.support) : b.toWeightBasis.repr (P.root i) = Finsupp.single i 1 := by
  simp [← LinearEquiv.eq_symm_apply]

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