squarefree_and_prime_pow_iff_prime

English

A number n is squarefree and a prime power if and only if n is prime.

Русский

Число n квадратносвободно и является простым основанием степени тогда и только тогда, когда n простое.

LaTeX

$$$\\text{Squarefree}(n) \\land \\text{IsPrimePow}(n) \\iff \\text{Prime}(n)$$$

Lean4

theorem squarefree_and_prime_pow_iff_prime {n : ℕ} : Squarefree n ∧ IsPrimePow n ↔ Prime n :=
  by
  refine ⟨?_, fun hn => ⟨hn.squarefree, hn.isPrimePow⟩⟩
  rw [isPrimePow_nat_iff]
  rintro ⟨h, p, k, hp, hk, rfl⟩
  rw [squarefree_pow_iff hp.ne_one hk.ne'] at h
  rwa [h.2, pow_one]

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