factorization_le_of_le_pow — Mathlib

English

If n ≤ p^b, then the exponent of p in the factorization of n is at most b: ν_p(n) ≤ b.

Русский

Если n ≤ p^b, то показатель степени p в факторизации n не превосходит b: ν_p(n) ≤ b.

LaTeX

$$$$n \le p^{b} \Rightarrow \nu_{p}(n) \le b.$$$$

Lean4

/-- An upper bound on `n.factorization p` -/
theorem factorization_le_of_le_pow {n p b : ℕ} (hb : n ≤ p ^ b) : n.factorization p ≤ b := by
  if hn : n = 0 then simp [hn]
  else
    if pp : p.Prime then exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
    else simp [factorization_eq_zero_of_non_prime n pp]

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