isCoprime_iff — Mathlib

English

For natural numbers m,n, IsCoprime m n is equivalent to m = 1 or n = 1.

Русский

Для натуральных чисел m, n утверждение IsCoprime m n эквивалентно m = 1 или n = 1.

LaTeX

$$$\operatorname{IsCoprime}(m, n) \iff (m = 1 \lor n = 1)$$$

Lean4

/-- `IsCoprime` is not a useful definition for `Nat`; consider using `Nat.Coprime` instead. -/
@[simp]
theorem isCoprime_iff {m n : ℕ} : IsCoprime m n ↔ m = 1 ∨ n = 1 :=
  by
  refine ⟨fun ⟨a, b, H⟩ => ?_, fun h => ?_⟩
  · simp_rw [Nat.add_eq_one_iff, mul_eq_one, mul_eq_zero] at H
    exact H.symm.imp (·.1.2) (·.2.2)
  · obtain rfl | rfl := h
    · exact isCoprime_one_left
    · exact isCoprime_one_right

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