α : Type u_2
M : Type u_1
N : Type ?u.43675
P : Type ?u.43678
R : Type u_3
S : Type ?u.43684
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set M
a : α
⊢ span R (single a '' s) = span R (↑(lsingle a) '' s)
α : Type u_2
M : Type u_1
N : Type ?u.43675
P : Type ?u.43678
R : Type u_3
S : Type ?u.43684
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set M
a : α
⊢ span R (single a '' s) = map (lsingle a) (span R s)
rw [← span_image]
no goals
α : Type u_2
M : Type u_1
N : Type ?u.43675
P : Type ?u.43678
R : Type u_3
S : Type ?u.43684
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s : Set M
a : α
⊢ span R (single a '' s) = span R (↑(lsingle a) '' s)
rfl