English
Equivalence of linear independence on s and on its image under an injective linear map.
Русский
Эквивалентность линейной независимости на s и на образе под инъективным линейным отображением.
LaTeX
$$$\\\\mathrm{LinearIndepOn}_R (f \\circ v) s \\\\iff \\\\mathrm{LinearIndepOn}_R v (\\operatorname{image} f \, s).$$$
Lean4
/-- If `f` is a linear map injective on the span of the range of `v`, then the family `f ∘ v`
is linearly independent if and only if the family `v` is linearly independent.
See `LinearMap.linearIndependent_iff_of_disjoint` for the version with `Set.InjOn` replaced
by `Disjoint` when working over a ring. -/
protected theorem linearIndependent_iff_of_injOn (f : M →ₗ[R] M') (hf_inj : Set.InjOn f (span R (Set.range v))) :
LinearIndependent R (f ∘ v) ↔ LinearIndependent R v :=
by
simp_rw [LinearIndependent, Finsupp.linearCombination_linear_comp, coe_comp]
rw [hf_inj.injective_iff]
rw [← Finsupp.range_linearCombination, LinearMap.coe_range]
