factorization_factorial_eq_zero_of_lt

English

If n < p, then (n)! has zero exponent of p in its factorization.

Русский

Если n < p, то у n! по p-й факторизации нет факторов p (равно нулю).

LaTeX

$$$ (n)!.factorization p = 0 \\quad\\text{если } n < p. $$$

Lean4

theorem factorization_factorial_eq_zero_of_lt (h : n < p) : (factorial n).factorization p = 0 := by
  induction n with
  | zero => simp
  | succ n hn =>
    rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add, Pi.add_apply,
      hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]

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