notMem_nonZeroDivisorsRight_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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