noZeroDivisors_iff_eq_zero_of_mul

English

NoZeroDivisors is equivalent to: for all a ≠ 0, and ∀ y, x·y = 0 → y = 0 and ∀ y, y·x = 0 → y = 0.

Русский

NoZeroDivisors эквивалентно: для всех a ≠ 0 и всех y: a·y = 0 → y = 0 и для всех y: y·a = 0 → y = 0.

LaTeX

$$$\text{NoZeroDivisors}(M_0) \iff \forall a\,(a\neq 0) \Rightarrow (\forall y, a\cdot y = 0 \Rightarrow y = 0) \land (\forall y, y \cdot a = 0 \Rightarrow y = 0)$$$

Lean4

theorem noZeroDivisors_iff_eq_zero_of_mul :
    NoZeroDivisors M₀ ↔ ∀ x : M₀, x ≠ 0 → (∀ y, x * y = 0 → y = 0) ∧ (∀ y, y * x = 0 → y = 0) := by
  simp only [forall_and, ← noZeroDivisors_iff_right_eq_zero_of_mul, ← noZeroDivisors_iff_left_eq_zero_of_mul, and_self]

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