English
For any p in a CancelCommMonoidWithZero M and n ∈ N, Prime(p^n) holds iff Prime p and n=1.
Русский
Для любого p в CancelCommMonoidWithZero M и n ∈ N: Prime(p^n) ⇔ Prime p и n=1.
LaTeX
$$$ [CancelCommMonoidWithZero M] {p : M} {n : \mathbb{N}} : Prime (p ^ n) \leftrightarrow (Prime p \land n = 1) $$$
Lean4
@[simp]
theorem prime_pow_iff [CancelCommMonoidWithZero M] {p : M} {n : ℕ} : Prime (p ^ n) ↔ Prime p ∧ n = 1 :=
by
refine ⟨fun hp ↦ ?_, fun ⟨hp, hn⟩ ↦ by simpa [hn]⟩
suffices n = 1 by simp_all
rcases n with - | n
· simp at hp
· rw [Nat.succ.injEq]
rw [pow_succ', prime_mul_iff] at hp
rcases hp with ⟨hp, hpn⟩ | ⟨hp, hpn⟩
· by_contra contra
rw [isUnit_pow_iff contra] at hpn
exact hp.not_unit hpn
· exfalso
exact hpn.not_unit (hp.pow n)
