isCoprime_iff — Mathlib

English

In a semifield, IsCoprime m n is equivalent to m ≠ 0 ∨ n ≠ 0.

Русский

В полуполе IsCoprime m n эквивалентно m ≠ 0 или n ≠ 0.

LaTeX

$$$\operatorname{IsCoprime}(m, n) \iff (m \neq 0 \lor n \neq 0)$$$

Lean4

/-- `IsCoprime` is not a useful definition if an inverse is available. -/
@[simp]
theorem isCoprime_iff {R : Type*} [Semifield R] {m n : R} : IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0 :=
  by
  obtain rfl | hn := eq_or_ne n 0
  · simp [isCoprime_zero_right]
  suffices IsCoprime m n by simpa [hn]
  refine ⟨0, n⁻¹, ?_⟩
  simp [inv_mul_cancel₀ hn]

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