English
IsPrimePow n is equivalent to n = p^k for some prime p and k ≥ 1, i.e., n has a prime factorization consisting of a single prime.
Русский
IsPrimePow n эквивалентно n = p^k для некоторого простого p и k ≥ 1, то есть в факторизации n присутствует ровно один простейший множитель.
LaTeX
$$$\text{IsPrimePow}(n) \iff \exists p\;\exists k>0:\ n=p^k.$$$
Lean4
/-- For any multiplicative function `f` with `f 1 = 1` and any `n ≠ 0`,
we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n` -/
theorem multiplicative_factorization {β : Type*} [CommMonoid β] (f : ℕ → β)
(h_mult : ∀ x y : ℕ, Coprime x y → f (x * y) = f x * f y) (hf : f 1 = 1) :
∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k) :=
by
apply Nat.recOnPosPrimePosCoprime
· rintro p k hp - -
simp [Prime.factorization_pow hp, Finsupp.prod_single_index _, hf]
· simp
· rintro -
rw [factorization_one, hf]
simp
· intro a b _ _ hab ha hb hab_pos
rw [h_mult a b hab, ha (left_ne_zero_of_mul hab_pos), hb (right_ne_zero_of_mul hab_pos),
factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]
exact hab.disjoint_primeFactors
