R : Type u_1
R₂ : Type u_2
K : Type ?u.203558
M : Type u_3
M₂ : Type u_4
V : Type ?u.203567
S : Type ?u.203570
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
x✝ : M
p p' : Submodule R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
s✝ t : Set M
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : x ∈ span R s
⊢ ↑f x ∈ map f (span R s)
R : Type u_1
R₂ : Type u_2
K : Type ?u.203558
M : Type u_3
M₂ : Type u_4
V : Type ?u.203567
S : Type ?u.203570
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
x✝ : M
p p' : Submodule R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
s✝ t : Set M
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : x ∈ span R s
⊢ ↑f x ∈ span R₂ (↑f '' s)
rw [Submodule.span_image]
no goals
R : Type u_1
R₂ : Type u_2
K : Type ?u.203558
M : Type u_3
M₂ : Type u_4
V : Type ?u.203567
S : Type ?u.203570
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
x✝ : M
p p' : Submodule R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
s✝ t : Set M
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
x : M
s : Set M
h : x ∈ span R s
⊢ ↑f x ∈ map f (span R s)
exact Submodule.mem_map_of_mem h