English
In a commutative semiring R, for any principal ideal I and element x ∈ I, x divides generator(I) if and only if I is the span of {x}.
Русский
В коммутативном полугруппе-предметах R для любой главной идеала I и элемента x ∈ I верно, что x делит порождающий I тогда и только тогда, когда I = ⟨x⟩.
LaTeX
$$$\\forall R [\\text{CommSemiring } R], \\forall I (I.I IsPrincipal) {x: R}, x \\in I \\Rightarrow (x \\mid generator I \\;\\leftrightarrow\\; I = \\langle x \\rangle).$$$
Lean4
theorem dvd_generator_iff {R : Type*} [CommSemiring R] {I : Ideal R} [I.IsPrincipal] {x : R} (hx : x ∈ I) :
x ∣ generator I ↔ I = Ideal.span { x } :=
by
simp_rw [le_antisymm_iff, I.span_singleton_le_iff_mem.2 hx, and_true, ← Ideal.mem_span_singleton]
conv_rhs => rw [← span_singleton_generator I, Submodule.span_singleton_le_iff_mem]
