English
Let (v_i) be a linearly independent family in a module over a ring R. For any finitely supported coefficient function l: ι →₀ R and any x in the span of the range of v, if x equals the linear combination ∑ i l(i) v_i, then the coordinate representation of x is precisely l.
Русский
Пусть (v_i) — линейно независимая семейство в модуле над R. Для любой конечноподдерживаемой функции коэффициентов l: ι →₀ R и любого x из порождающего подпространства образа v, если x равно линейной комбинации ∑ i l(i) v_i, тогда координатное представление x равно l.
LaTeX
$$$hv.repr\,x = l \quad\text{whenever}\quad Finsupp.linearCombination R v l = \uparrow x$$$
Lean4
theorem repr_eq {l : ι →₀ R} {x : span R (range v)} (eq : Finsupp.linearCombination R v l = ↑x) : hv.repr x = l :=
by
have :
↑((LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l) =
Finsupp.linearCombination R v l :=
rfl
have : (LinearIndependent.linearCombinationEquiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l = x :=
by
rw [eq] at this
exact Subtype.ext_iff.2 this
rw [← LinearEquiv.symm_apply_apply hv.linearCombinationEquiv l]
rw [← this]
rfl
