coprime_factorial_iff — Mathlib

English

If m ≠ 1, then m and n! are coprime exactly when n < m.minFac.

Русский

Если m ≠ 1, тогда m и n! взаимно просты тогда, когда n < m.minFac.

LaTeX

$$$\\\\forall {m n} \\\\in \\\\mathbb{N}, m \\\\neq 1 \\\\rightarrow (m \\\\mathrm{Coprime} n!) \\\\Leftrightarrow (n < m.\\\\minFac)$$$

Lean4

theorem coprime_factorial_iff {m n : ℕ} (hm : m ≠ 1) : m.Coprime n ! ↔ n < m.minFac :=
  by
  rw [← not_le, iff_not_comm, Nat.Prime.not_coprime_iff_dvd]
  constructor
  · intro h
    exact ⟨m.minFac, minFac_prime hm, minFac_dvd m, Nat.dvd_factorial (minFac_pos m) h⟩
  · rintro ⟨p, hp, hdvd, hdvd'⟩
    exact le_trans (minFac_le_of_dvd hp.two_le hdvd) (hp.dvd_factorial.mp hdvd')

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