notMem_nonZeroDivisors_iff — Mathlib

English

In a monoid with zero, an element r is not a nonzero divisor if and only if there exists a nonzero s with r s = 0 or s r = 0.

Русский

В моноиде с нулём элемент r не является не нулевым делителем слева тогда и только тогда, когда существует ненулевой s such that r s = 0 или s r = 0.

LaTeX

$$$ r \notin M_0^{0} \iff (\exists s : M_0, r s = 0 \land s \neq 0) \lor (\exists s : M_0, s r = 0 \land s \neq 0)$$$

Lean4

theorem notMem_nonZeroDivisors_iff : r ∉ M₀⁰ ↔ {s | r * s = 0 ∧ s ≠ 0}.Nonempty ∨ {s | s * r = 0 ∧ s ≠ 0}.Nonempty := by
  simp [-not_and, not_and_or, mem_nonZeroDivisors_iff, Set.nonempty_def]

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