no goals
R : Type ?u.969460
R₁ : Type ?u.969463
R₂ : Type ?u.969466
R₃ : Type ?u.969469
R₄ : Type ?u.969472
S : Type ?u.969475
K : Type u_1
K₂ : Type ?u.969481
M : Type ?u.969484
M' : Type ?u.969487
M₁ : Type ?u.969490
M₂ : Type ?u.969493
M₃ : Type ?u.969496
M₄ : Type ?u.969499
N : Type ?u.969502
N₂ : Type ?u.969505
ι : Type ?u.969508
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
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p
classical by_cases h : a = 0 <;> simp [h, map_smul]
no goals
R : Type ?u.969460
R₁ : Type ?u.969463
R₂ : Type ?u.969466
R₃ : Type ?u.969469
R₄ : Type ?u.969472
S : Type ?u.969475
K : Type u_1
K₂ : Type ?u.969481
M : Type ?u.969484
M' : Type ?u.969487
M₁ : Type ?u.969490
M₂ : Type ?u.969493
M₃ : Type ?u.969496
M₄ : Type ?u.969499
N : Type ?u.969502
N₂ : Type ?u.969505
ι : Type ?u.969508
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
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p
by_cases h : a = 0 <;> simp [h, map_smul]