notMem_nonZeroDivisorsLeft_iff — Mathlib

English

An element x not in the left non-zero divisors of M₀ iff there exists a y ≠ 0 with x y = 0.

Русский

Элемент x не является левым нулевым делителем M₀ тогда и только тогда существует y ≠ 0 с x y = 0.

LaTeX

$$$ x \notin \operatorname{nonZeroDivisorsLeft}(M_0) \iff \{ y \mid x y = 0 \wedge y \neq 0 \}.\text{Nonempty}$$$

Lean4

theorem notMem_nonZeroDivisorsLeft_iff : x ∉ nonZeroDivisorsLeft M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty := by
  simpa [mem_nonZeroDivisorsLeft_iff] using Set.nonempty_def.symm

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