R : Type u_1
R₂ : Type u_2
K : Type ?u.11034
M : Type u_3
M₂ : Type u_4
V : Type ?u.11043
S : Type ?u.11046
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₂
s : Set M
N : Submodule R₂ M₂
⊢ s ⊆ ↑f ⁻¹' ↑N ↔ ∀ (m : M), m ∈ s → ↑f m ∈ N
R : Type u_1
R₂ : Type u_2
K : Type ?u.11034
M : Type u_3
M₂ : Type u_4
V : Type ?u.11043
S : Type ?u.11046
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₂
s : Set M
N : Submodule R₂ M₂
⊢ map f (span R s) ≤ N ↔ ∀ (m : M), m ∈ s → ↑f m ∈ N
rw [f.map_span, span_le, Set.image_subset_iff]
no goals
R : Type u_1
R₂ : Type u_2
K : Type ?u.11034
M : Type u_3
M₂ : Type u_4
V : Type ?u.11043
S : Type ?u.11046
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₂
s : Set M
N : Submodule R₂ M₂
⊢ s ⊆ ↑f ⁻¹' ↑N ↔ ∀ (m : M), m ∈ s → ↑f m ∈ N
exact Iff.rfl