dvd — Mathlib

English

If n is a prime power and m divides n with m ≠ 1, then m is a prime power.

Русский

Если n — простая степень, и m делит n при m ≠ 1, то m также является простой степенью.

LaTeX

$$$\forall n,m \in \mathbb{N}, IsPrimePow(n) \land m \mid n \land m \neq 1 \Rightarrow IsPrimePow(m)$$$

Lean4

theorem dvd {n m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m ≠ 1) : IsPrimePow m := by
  grind [isPrimePow_nat_iff, Nat.dvd_prime_pow, Nat.pow_eq_one]

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