R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
x : M
hx : x ∈ N
⊢ ∃ y yN, ↑ϕ { val := y, property := (_ : y ∈ O) } = ↑ϕ { val := x, property := (_ : x ∈ O) }
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
x : M
hx : x ∈ N
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ϕ { val := x, property := (_ : x ∈ O) }
rw [← mem_iff_generator_dvd, LinearMap.mem_submoduleImage_of_le hNO]
no goals
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
x : M
hx : x ∈ N
⊢ ∃ y yN, ↑ϕ { val := y, property := (_ : y ∈ O) } = ↑ϕ { val := x, property := (_ : x ∈ O) }
exact ⟨x, hx, rfl⟩