Prime powers and factorizations #
This file deals with factorizations of prime powers.
theorem
isPrimePow_of_minFac_pow_factorization_eq
{n : ℕ}
(h : n.minFac ^ n.factorization n.minFac = n)
(hn : n ≠ 1)
:
theorem
IsPrimePow.exists_ordCompl_eq_one
{n : ℕ}
(h : IsPrimePow n)
:
∃ (p : ℕ), Nat.Prime p ∧ n / p ^ n.factorization p = 1
@[deprecated IsPrimePow.exists_ordCompl_eq_one (since := "2024-10-24")]
theorem
IsPrimePow.exists_ord_compl_eq_one
{n : ℕ}
(h : IsPrimePow n)
:
∃ (p : ℕ), Nat.Prime p ∧ n / p ^ n.factorization p = 1
Alias of IsPrimePow.exists_ordCompl_eq_one
.
@[deprecated exists_ordCompl_eq_one_iff_isPrimePow (since := "2024-10-24")]
Alias of exists_ordCompl_eq_one_iff_isPrimePow
.
An equivalent definition for prime powers: n
is a prime power iff there is a unique prime
dividing it.
@[simp]
@[simp]