instDecidableRelIntIsCoprime — Mathlib

English

In the integer setting, IsCoprime is equivalent to gcd equals 1; this yields a decision procedure for coprimality of integers.

Русский

В целочисленном случае IsCoprime эквивалентно gcd = 1, что дает решение о приемлемости взаимной простоты.

LaTeX

$$$\forall m\,\forall n:\ IsCoprime\ m\ n \iff gcd(m,n) = 1$$$

Lean4

instance : DecidableRel (IsCoprime : ℤ → ℤ → Prop) := fun m n =>
  decidable_of_iff (Int.gcd m n = 1) Int.isCoprime_iff_gcd_eq_one.symm

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