noZeroDivisors_iff_left_eq_zero_of_mul

English

NoZeroDivisors implies: x ≠ 0 and y · x = 0 implies y = 0 for all x ≠ 0.

Русский

NoZeroDivisors =>: для любого x ≠ 0, если y·x = 0, то y = 0.

LaTeX

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

Lean4

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

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