dvd_factorial — Mathlib

English

For a prime p, p divides n! exactly when p ≤ n.

Русский

Для простого p делит ли факториал n! ровно тогда, когда p ≤ n.

LaTeX

$$$\\\\forall {n p : \\mathbb{N}} (\\\\text{Prime}(p)) \\\\rightarrow (p \\\\mid n! \\\\Leftrightarrow p \\\\le n)$$$

Lean4

theorem dvd_factorial : ∀ {n p : ℕ} (_ : Prime p), p ∣ n ! ↔ p ≤ n
  | 0, _, hp => iff_of_false hp.not_dvd_one (not_le_of_gt hp.pos)
  | n + 1, p, hp => by
    rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]
    exact
      ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
        (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩

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