isPrimePow_of_minFac_pow_factorization_eq

English

If the equation minFac^factorization(minFac) = n holds and n ≠ 1, then n is a prime power.

Русский

Если minFac^factorization(minFac) = n и n ≠ 1, тогда n — простая степень.

LaTeX

$$$(minFac^n.factorization(minFac)=n) \Rightarrow IsPrimePow(n)$, for n ≠ 1.$$

Lean4

theorem isPrimePow_of_minFac_pow_factorization_eq {n : ℕ} (h : n.minFac ^ n.factorization n.minFac = n) (hn : n ≠ 1) :
    IsPrimePow n := by
  rcases eq_or_ne n 0 with (rfl | hn')
  · simp_all
  refine ⟨_, _, (Nat.minFac_prime hn).prime, ?_, h⟩
  simp [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.support_factorization, hn', Nat.minFac_prime hn, Nat.minFac_dvd]

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