smoothNumbers_coprime — Mathlib

English

Let p be a prime and n be p-smooth. Then gcd(p,n) = 1.

Русский

Пусть p — простое число, n — p-гладкое. Тогда gcd(p,n) = 1.

LaTeX

$$$p \\text{ prime} \\land n \\in \\mathrm{smoothNumbers}(p) \\Rightarrow \\gcd(p,n) = 1$$$

Lean4

/-- If `p` is a prime and `n` is `p`-smooth, then `p` and `n` are coprime. -/
theorem smoothNumbers_coprime {p n : ℕ} (hp : p.Prime) (hn : n ∈ smoothNumbers p) : Nat.Coprime p n :=
  by
  simp only [smoothNumbers_eq_factoredNumbers] at hn
  exact hp.factoredNumbers_coprime Finset.notMem_range_self hn

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