eq_prime_pow_of_unique_prime_dvd — Mathlib

English

If n ≠ 0 and every prime divisor d of n equals p, then n = p^{length(n.primeFactorsList)}.

Русский

Если n ≠ 0 и каждый простой делитель d n равен p, то n = p^{length(n.primeFactorsList)}.

LaTeX

$$n \neq 0 \rightarrow (\forall d, Prime(d) \rightarrow d \mid n \rightarrow d = p) \rightarrow n = p^{n.primeFactorsList.length}$$

Lean4

theorem eq_prime_pow_of_unique_prime_dvd {n p : ℕ} (hpos : n ≠ 0) (h : ∀ {d}, Nat.Prime d → d ∣ n → d = p) :
    n = p ^ n.primeFactorsList.length := by
  set k := n.primeFactorsList.length
  rw [← prod_primeFactorsList hpos, ← prod_replicate k p,
    eq_replicate_of_mem fun d hd => h (prime_of_mem_primeFactorsList hd) (dvd_of_mem_primeFactorsList hd)]

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