English
The lemma basis_repr asserts the explicit compatibility of basis repr with the construction; it states how the representation map evaluates on g at index ix.
Русский
Лемма basis_repr утверждает явную совместимость представления базы с построением; описывается как значение отображения представления на g в позиции ix.
LaTeX
$$$\\bigl(\\mathrm{Finsupp}.basis\\, b\\bigr).\\mathrm{repr}\\; g\\; i_x = (b_{i_x.1}).\\mathrm{repr}}(g_{i_x.1})\\; i_x.2$$$
Lean4
/-- For any `r : R`, `s : S`, we have
`B.repr ((algebra_map R S r) * s) i = r * (B.repr s i) `. -/
theorem repr_smul' (i : ι) (r : R) (s : S) : B.repr (algebraMap R S r * s) i = r * B.repr s i := by
rw [← smul_eq_mul, ← smul_eq_mul, algebraMap_smul, map_smul, Finsupp.smul_apply]
