coprime_descFactorial_of_lt_of_le

English

If p is prime, n < p, and k ≤ n, then p is coprime to n.descFactorial(k).

Русский

Если p простое, n < p, и k ≤ n, то p взаимно с n.descFactorial(k).

LaTeX

$$$\\\\forall {p n k} \\\\in \\\\mathbb{N}, (\\\\mathrm{Prime}(p)) \\\\rightarrow (n < p) \\\\rightarrow (k \\le n) \\\\Rightarrow p \\\\mathrm{Coprime} (n.descFactorial k)$$$

Lean4

theorem coprime_descFactorial_of_lt_of_le {p n k : ℕ} (hp : p.Prime) (hn : n < p) (hk : k ≤ n) :
    p.Coprime (n.descFactorial k) := by
  rw [Nat.descFactorial_eq_div hk]
  refine (hp.coprime_factorial_of_lt hn).coprime_div_right ?_
  simp [Nat.factorial_dvd_factorial]

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