English
For bases b and b', coordinates transform via a sum identity: for each i, sum_j b.repr(b' j) i · b'.repr x j = b.repr x i.
Русский
Координаты преобразуются через тождество: для всех i выполняется сумма по j: b.repr(b' j) i · b'.repr x j = b.repr x i.
LaTeX
$$$\\sum_{j} b'.\\mathrm{repr}\\, x\\, j \\cdot b.\\mathrm{repr}(b' j)\\, i = b.\\mathrm{repr} x\\, i.$$$
Lean4
theorem constr_range {f : ι → M'} : LinearMap.range (constr (M' := M') b S f) = span R (range f) := by
rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ← Finsupp.supported_univ,
Finsupp.lmapDomain_supported, ← Set.image_univ, ← Finsupp.span_image_eq_map_linearCombination, Set.image_id]
