no goals
R : Type ?u.960022
R₁ : Type ?u.960025
R₂ : Type ?u.960028
R₃ : Type ?u.960031
R₄ : Type ?u.960034
S : Type ?u.960037
K : Type u_1
K₂ : Type ?u.960043
M : Type ?u.960046
M' : Type ?u.960049
M₁ : Type ?u.960052
M₂ : Type ?u.960055
M₃ : Type ?u.960058
M₄ : Type ?u.960061
N : Type ?u.960064
N₂ : Type ?u.960067
ι : Type ?u.960070
V : Type u_2
V₂ : Type u_3
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ map (a • f) p ≤ map f p
rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap]
no goals
R : Type ?u.960022
R₁ : Type ?u.960025
R₂ : Type ?u.960028
R₃ : Type ?u.960031
R₄ : Type ?u.960034
S : Type ?u.960037
K : Type u_1
K₂ : Type ?u.960043
M : Type ?u.960046
M' : Type ?u.960049
M₁ : Type ?u.960052
M₂ : Type ?u.960055
M₃ : Type ?u.960058
M₄ : Type ?u.960061
N : Type ?u.960064
N₂ : Type ?u.960067
ι : Type ?u.960070
V : Type u_2
V₂ : Type u_3
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ map f p ≤ map (a • f) p
rw [map_le_iff_le_comap, ← comap_smul f _ a h, ← map_le_iff_le_comap]