exists_eq_span_pair — Mathlib

English

In a Dedekind domain, every nonzero ideal I is generated by two elements: there exist x ∈ I, y ∈ R with I = ⟨x,y⟩.

Русский

В Дедекдиновом домене любой ненулевой идеал I порожден двумя элементами: найдутся x ∈ I, y ∈ R такие, что I = (x,y).

LaTeX

$$$\forall I\; (I \neq 0),\; ∃ x,y: R,\; I = \langle x,y\rangle.$$$

Lean4

/-- In a Dedekind domain, any ideal is spanned by two elements, where one of the element
could be any fixed non-zero element in the ideal. -/
theorem exists_eq_span_pair {I : Ideal R} {x : R} (hxI : x ∈ I) (hx : x ≠ 0) : ∃ y, I = .span { x, y } :=
  by
  obtain ⟨y, rfl⟩ := exists_sup_span_eq (I.span_singleton_le_iff_mem.mpr hxI) (by simpa)
  simp_rw [← Ideal.span_union, Set.union_singleton, Set.pair_comm x]
  use y

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