eq_of_mul_eq_zero — Mathlib

English

If m and n are coprime and mn = 0, then either m = 0 and n = 1 or m = 1 and n = 0.

Русский

Если m и n взаимно просты и mn = 0, то либо m = 0 и n = 1, либо m = 1 и n = 0.

LaTeX

$$$\forall m,n \in \mathbb{N}, (\gcd(m,n) = 1) \land (m n = 0) \Rightarrow ((m=0 \land n=1) \lor (m=1 \land n=0))$$$

Lean4

theorem eq_of_mul_eq_zero {m n : ℕ} (h : m.Coprime n) (hmn : m * n = 0) : m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 :=
  (Nat.mul_eq_zero.mp hmn).imp (fun hm => ⟨hm, n.coprime_zero_left.mp <| hm ▸ h⟩) fun hn =>
    let eq := hn ▸ h.symm
    ⟨m.coprime_zero_left.mp <| eq, hn⟩

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