R : Type u
M : Type v
F : Type ?u.162652
G : Type ?u.162655
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I✝ J : Ideal R
N P : Submodule R M
S✝ : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : x ∈ comap f S
⊢ r • x ∈ comap f (I • S)
R : Type u
M : Type v
F : Type ?u.162652
G : Type ?u.162655
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I✝ J : Ideal R
N P : Submodule R M
S✝ : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
⊢ I • comap f S ≤ comap f (I • S)
refine' Submodule.smul_le.mpr fun r hr x hx => _
R : Type u
M : Type v
F : Type ?u.162652
G : Type ?u.162655
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I✝ J : Ideal R
N P : Submodule R M
S✝ : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : ↑f x ∈ S
⊢ ↑f (r • x) ∈ I • S
R : Type u
M : Type v
F : Type ?u.162652
G : Type ?u.162655
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I✝ J : Ideal R
N P : Submodule R M
S✝ : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : x ∈ comap f S
⊢ r • x ∈ comap f (I • S)
rw [Submodule.mem_comap] at hx⊢
R : Type u
M : Type v
F : Type ?u.162652
G : Type ?u.162655
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I✝ J : Ideal R
N P : Submodule R M
S✝ : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : ↑f x ∈ S
⊢ r • ↑f x ∈ I • S
R : Type u
M : Type v
F : Type ?u.162652
G : Type ?u.162655
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I✝ J : Ideal R
N P : Submodule R M
S✝ : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : ↑f x ∈ S
⊢ ↑f (r • x) ∈ I • S
rw [f.map_smul]
no goals
R : Type u
M : Type v
F : Type ?u.162652
G : Type ?u.162655
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
I✝ J : Ideal R
N P : Submodule R M
S✝ : Set R
T : Set M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : ↑f x ∈ S
⊢ r • ↑f x ∈ I • S
exact Submodule.smul_mem_smul hr hx