mem_principal_ideals_iff — Mathlib

English

More generally, I belongs to the principal-ideals range if and only if there exists x such that Span of x equals I.

Русский

Более общо, I принадлежит образу главных идеалов тогда и только тогда, когда существует x такой, что Span(x) = I.

LaTeX

$$I ∈ (toPrincipalIdeal R K).range \iff ∃ x : K, spanSingleton R⁰ x = I$$

Lean4

theorem mem_principal_ideals_iff {I : (FractionalIdeal R⁰ K)ˣ} :
    I ∈ (toPrincipalIdeal R K).range ↔ ∃ x : K, spanSingleton R⁰ x = I :=
  by
  simp only [MonoidHom.mem_range, toPrincipalIdeal_eq_iff]
  constructor <;> rintro ⟨x, hx⟩
  · exact ⟨x, hx⟩
  · refine ⟨Units.mk0 x ?_, hx⟩
    rintro rfl
    simp [I.ne_zero.symm] at hx

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