factorization_minFac_ne_zero — Mathlib

English

If n is a prime power, then the exponent of its smallest prime factor in its prime factorization is nonzero (positive).

Русский

Пусть n — степень простого. В разложении n по простым множителям показатель степени минимального простого числа положителен.

LaTeX

$$$\operatorname{IsPrimePow}(n) \Rightarrow n("minFac") \text{ существует и } n.\text{factorization}(n.minFac) \neq 0$$$

Lean4

@[deprecated Nat.factorization_minFac_ne_zero (since := "2025-07-21")]
theorem factorization_minFac_ne_zero {n : ℕ} (hn : IsPrimePow n) : n.factorization n.minFac ≠ 0 :=
  Nat.factorization_minFac_ne_zero (one_lt hn)

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