factorization_centralBinom_of_two_mul_self_lt_three_mul

English

Primes larger than about 2n/3 but less than n do not appear in the factorization of centralBinom n.

Русский

Простые больше примерно 2n/3 и меньше n не входят в факторизацию centralBinom n.

LaTeX

$$$ (\\text{centralBinom } n).factorization p = 0 \\quad\\text{if } p > \\frac{2n}{3} \\text{ and } p ≤ n. $$$

Lean4

/-- Primes greater than about `2 * n / 3` and less than `n` do not appear in the factorization of
`centralBinom n`. -/
theorem factorization_centralBinom_of_two_mul_self_lt_three_mul (n_big : 2 < n) (p_le_n : p ≤ n) (big : 2 * n < 3 * p) :
    (centralBinom n).factorization p = 0 :=
  by
  refine factorization_choose_of_lt_three_mul ?_ p_le_n (p_le_n.trans ?_) big
  · cutsat
  · rw [two_mul, add_tsub_cancel_left]

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