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')