no goals
R : Type ?u.1515248
R₁ : Type ?u.1515251
R₂ : Type ?u.1515254
R₃ : Type ?u.1515257
R₄ : Type ?u.1515260
S : Type ?u.1515263
K : Type u_1
K₂ : Type ?u.1515269
M : Type ?u.1515272
M' : Type ?u.1515275
M₁ : Type ?u.1515278
M₂ : Type ?u.1515281
M₃ : Type ?u.1515284
M₄ : Type ?u.1515287
N : Type ?u.1515290
N₂ : Type ?u.1515293
ι : Type ?u.1515296
V : Type u_2
V₂ : Type u_3
inst✝⁵ : Semifield K
inst✝⁴ : Semifield K₂
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
⊢ range (a • f) = ⨆ (_ : a ≠ 0), range f
simpa only [range_eq_map] using Submodule.map_smul' f _ a