English
For any family (f_i) with each f_i LI, the map ix ↦ DFinsupp.single ix.1 (f_ix.1 ix.2) is LI.
Русский
Если каждое f_i линейно независимо, тогда отображение ix ↦ \n DFinsupp.single ix.1 (f_ix.1 ix.2) линейно независимо.
LaTeX
$$$\\text{LinearIndependent } R\\;\\bigl(\\lambda ix. \\mathrm{DFinsupp}.single_{ix.1}(f_{ix.1}(ix.2))\\bigr)$$$
Lean4
theorem trans {R S M : Type*} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M]
[IsScalarTower R S M] [Module.Free S M] [Module.Free R S] : Module.Free R M :=
let e : (ChooseBasisIndex S M →₀ S) ≃ₗ[R] ChooseBasisIndex S M →₀ (ChooseBasisIndex R S →₀ R) :=
Finsupp.mapRange.linearEquiv (chooseBasis R S).repr
let e : M ≃ₗ[R] ChooseBasisIndex S M →₀ (ChooseBasisIndex R S →₀ R) := (chooseBasis S M).repr.restrictScalars R ≪≫ₗ e
.of_equiv e.symm
