R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst✝ : IsPrincipal (map ϕ N)
x : M
hx : x ∈ N
⊢ ∃ y, y ∈ N ∧ ↑ϕ y = ↑ϕ x
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst✝ : IsPrincipal (map ϕ N)
x : M
hx : x ∈ N
⊢ generator (map ϕ N) ∣ ↑ϕ x
rw [← mem_iff_generator_dvd, Submodule.mem_map]
no goals
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst✝ : IsPrincipal (map ϕ N)
x : M
hx : x ∈ N
⊢ ∃ y, y ∈ N ∧ ↑ϕ y = ↑ϕ x
exact ⟨x, hx, rfl⟩