le_two_mul_of_factorization_centralBinom_pos

English

If a prime p has positive multiplicity in centralBinom n, then p ≤ 2n.

Русский

Если простое p встречается в v_p(centralBinom n) больше нуля, то p ≤ 2n.

LaTeX

$$$ 0 < (\\text{centralBinom } n).factorization p \\Rightarrow p \\le 2n. $$$

Lean4

/-- Contrapositive form of `Nat.factorization_centralBinom_eq_zero_of_two_mul_lt` -/
theorem le_two_mul_of_factorization_centralBinom_pos (h_pos : 0 < (centralBinom n).factorization p) : p ≤ 2 * n :=
  le_of_not_gt (pos_iff_ne_zero.mp h_pos ∘ factorization_centralBinom_eq_zero_of_two_mul_lt)

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