pow — Mathlib

English

If n is prime power and k ≠ 0, then n^k is also a prime power.

Русский

Если n — степень простого, и k ≠ 0, тогда n^k — тоже степень простого.

LaTeX

$$$\text{IsPrimePow } n \rightarrow (k \neq 0) \rightarrow \text{IsPrimePow } (n^k)$$$

Lean4

theorem pow {n : R} (hn : IsPrimePow n) {k : ℕ} (hk : k ≠ 0) : IsPrimePow (n ^ k) :=
  let ⟨p, k', hp, hk', hn⟩ := hn
  ⟨p, k * k', hp, mul_pos hk.bot_lt hk', by rw [pow_mul', hn]⟩

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