English
In a commutative NoZeroDivisors semiring, span{r} ∈ nonZeroDivisors iff r ∈ nonZeroDivisors.
Русский
В коммутативном кольце без делителей нуля, span{r} принадлежит множеству ненулевых делителей тогда и только тогда, когда r тоже является ненулевым делителем.
LaTeX
$$$\\operatorname{span}\\{r\\} \\in (\\operatorname{nonZeroDivisors} \\; R) \\iff r \\in (\\operatorname{nonZeroDivisors} \\; R)$$$
Lean4
theorem span_singleton_nonZeroDivisors {R : Type*} [CommSemiring R] [NoZeroDivisors R] {r : R} :
span { r } ∈ (Ideal R)⁰ ↔ r ∈ R⁰ := by
cases subsingleton_or_nontrivial R
· simp_rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
exact ⟨fun _ _ _ ↦ Subsingleton.eq_zero _, fun _ _ _ ↦ Subsingleton.eq_zero _⟩
· rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot, span_singleton_eq_bot]
