English
For the basis built from bases b_i, the representation map evaluated at g and index ix equals (b_{ix.1}).repr (g_{ix.1}) (ix.2).
Русский
Для базиса, построенного из базисов b_i, отображение представления на элемент g и индекс ix даёт значение (b_{ix.1}).repr (g_{ix.1}) (ix.2).
LaTeX
$$$(\\mathrm{Finsupp}.basis\\; b).\\mathrm{repr}\; g\\; i_x = (b_{i_x.1}).\\mathrm{repr}(g_{i_x.1})\\; i_x.2$$$
Lean4
@[simp]
theorem basis_repr {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) (g : ι →₀ M) (ix) :
(Finsupp.basis b).repr g ix = (b ix.1).repr (g ix.1) ix.2 :=
rfl