generator_submoduleImage_dvd_of_mem

English

In a Bézout ring, the ideal generated by {x,y} is principal.

Русский

В кольце Безо, идеал, порожденный {x,y}, главен.

LaTeX

$$IsPrincipal (Ideal.span (Set.insert x (Set.singleton y)))$$

Lean4

theorem generator_submoduleImage_dvd_of_mem {N O : Submodule R M} (hNO : N ≤ O) (ϕ : O →ₗ[R] R)
    [(ϕ.submoduleImage N).IsPrincipal] {x : M} (hx : x ∈ N) : generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, hNO hx⟩ :=
  by
  rw [← mem_iff_generator_dvd, LinearMap.mem_submoduleImage_of_le hNO]
  exact ⟨x, hx, rfl⟩

Похожие утверждения