gcd_eq_one_of_lt_minFac — Mathlib

English

Let n,m be natural numbers with m ≠ 0 and m < minFac(n). Then n.gcd(m) = 1.

Русский

Пусть n,m ∈ ℕ, m ≠ 0 и m < minFac(n). Тогда НОД(n,m) = 1.

LaTeX

$$$$ \forall n,m \in \mathbb{N},\ m \neq 0 \land m < \minFac(n) \Rightarrow \gcd(n,m) = 1. $$$$

Lean4

/-- If `0 < m < minFac n`, then `n` and `m` have gcd equal to `1`. -/
theorem gcd_eq_one_of_lt_minFac {n m : ℕ} (h₀ : m ≠ 0) (h : m < minFac n) : n.gcd m = 1 :=
  coprime_iff_gcd_eq_one.mp <| coprime_of_lt_minFac h₀ h

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