factorization_lt — Mathlib

English

For every nonzero n and every p, the exponent of p in the prime factorization of n is strictly less than n: ν_p(n) < n.

Русский

Для каждого непустого n и любого p показатель степени p в разложении n по простым удовлетворяет ν_p(n) < n.

LaTeX

$$$$\forall n\in\mathbb{N},\ n \neq 0 \Rightarrow \forall p\in\mathbb{N},\ \nu_p(n) < n.$$$$

Lean4

/-- A crude upper bound on `n.factorization p` -/
theorem factorization_lt {n : ℕ} (p : ℕ) (hn : n ≠ 0) : n.factorization p < n :=
  by
  by_cases pp : p.Prime
  · exact (Nat.pow_lt_pow_iff_right pp.one_lt).1 <| (ordProj_le p hn).trans_lt <| Nat.lt_pow_self pp.one_lt
  · simpa only [factorization_eq_zero_of_non_prime n pp] using hn.bot_lt

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