English
For a linear equivalence f: E ≃ₗ[K] F, the Z-span of the image of the basis under f equals the image of the Z-span of the original basis; i.e., Submodule.map preserves the Z-span along f.
Русский
Пусть f: E ≃ₗ[K] F — линейное эквивалентное отображение. Тогда Z-предел образа базиса под f равенобразному Z-пределу исходного базиса: отображение Z-предела сохраняется.
LaTeX
$$$\\mathrm{Submodule}.map (f|_{\\mathbb{Z}}) (\\operatorname{span}_{\\mathbb{Z}}(\\operatorname{range} b)) = \\operatorname{span}_{\\mathbb{Z}}(\\operatorname{range}(b.map f))$$$
Lean4
theorem map {F : Type*} [AddCommGroup F] [Module K F] (f : E ≃ₗ[K] F) :
Submodule.map (f.restrictScalars ℤ) (span ℤ (Set.range b)) = span ℤ (Set.range (b.map f)) := by
simp_rw [Submodule.map_span, LinearEquiv.restrictScalars_apply, Basis.coe_map, Set.range_comp]
