noZeroDivisors_iff_right_eq_zero_of_mul

English

For mul with a zero object, NoZeroDivisors is equivalent to: for all x ≠ 0, x·y=0 implies y=0 for all y and similarly on the left.

Русский

Для коллизий нулей эквивалентно: для всех x ≠ 0, если x·y=0, то y=0 и аналогично слева.

LaTeX

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

Lean4

theorem noZeroDivisors_iff_right_eq_zero_of_mul : NoZeroDivisors M₀ ↔ ∀ x : M₀, x ≠ 0 → ∀ y, x * y = 0 → y = 0 :=
  by
  simp only [noZeroDivisors_iff, or_iff_not_imp_left]
  exact ⟨fun h a ha b eq ↦ h eq ha, fun h a b eq ha ↦ h a ha b eq⟩

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