instNoZeroDivisors — Mathlib

English

In a Euclidean domain, if a·b = 0 then either a = 0 or b = 0.

Русский

В евклидовой области если a·b = 0, то либо a = 0, либо b = 0.

LaTeX

$$$a b = 0 \Rightarrow a = 0 \lor b = 0$$$

Lean4

instance (priority := 70) (R : Type*) [e : EuclideanDomain R] : NoZeroDivisors R :=
  haveI := Classical.decEq R
  {
    eq_zero_or_eq_zero_of_mul_eq_zero := fun {a b} h =>
      or_iff_not_and_not.2 fun h0 => h0.1 <| by rw [← mul_div_cancel_right₀ a h0.2, h, zero_div] }
    -- see Note [lower instance priority]

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