eq_pow_of_factorization_eq_single

English

If n ≠ 0 and its factorization is a single p with exponent k, then n = p^k.

Русский

Если n ≠ 0 и факторизация n содержит один простой p с показателем k, то n = p^k.

LaTeX

$$$ n \neq 0 \wedge n.factorization = \mathsf{single}(p,k) \Rightarrow n = p^k $$$

Lean4

/-- If the factorization of `n` contains just one number `p` then `n` is a power of `p` -/
theorem eq_pow_of_factorization_eq_single {n p k : ℕ} (hn : n ≠ 0) (h : n.factorization = Finsupp.single p k) :
    n = p ^ k := by
  rw [← Nat.factorization_prod_pow_eq_self hn, h]
  simp

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