minFac_pow_factorization_eq — Mathlib

English

If n is prime power, then n equals its minimal prime factor raised to its factorization power, i.e., n = minFac(n)^{factorization(n).minFac}.

Русский

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

LaTeX

$$$\text{minFac}^{\,n.factorization(minFac)} = n$ for IsPrimePow n.$$

Lean4

theorem minFac_pow_factorization_eq {n : ℕ} (hn : IsPrimePow n) : n.minFac ^ n.factorization n.minFac = n :=
  by
  obtain ⟨p, k, hp, hk, rfl⟩ := hn
  rw [← Nat.prime_iff] at hp
  rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]

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