factorization_centralBinom_eq_zero_of_two_mul_lt

English

If 2n < p, then (centralBinom n).factorization p = 0.

Русский

Если 2n < p, то v_p(centralBinom n) = 0.

LaTeX

$$$ (\\text{centralBinom } n).factorization p = 0 \\quad\\text{при } 2n < p. $$$

Lean4

/-- If a prime `p` has positive multiplicity in the `n`th central binomial coefficient,
`p` is no more than `2 * n` -/
theorem factorization_centralBinom_eq_zero_of_two_mul_lt (h : 2 * n < p) : (centralBinom n).factorization p = 0 :=
  factorization_choose_eq_zero_of_lt h

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