Arguments over prime factorizations in Lean: σ(n) = ∏ σ(q^k) as a Finset product

To reason about multiplicative functions prime by prime (Euler's odd perfect number form), first turn everything into Finset products over n.primeFactors. Use rw [IsMultiplicative.multiplicative_factorization _ isMultiplicative_sigma hn0, Finsupp.prod, Nat.support_factorization], which gives σ 1 n = ∏ q ∈ n.primeFactors, σ 1 (q ^ n.factorization q). Do the same for n itself with conv_lhs => rw [← Nat.prod_factorization_pow_eq_self hn0] (not factorization_prod_pow_eq_self, which takes a Finsupp). sigma_one_apply_prime_pow hp then gives the geometric sum. Split off one prime with mul_prod_erase s f hp, and get two distinct factors dividing the product from prod_dvd_prod_of_subset {p,q} s plus prod_pair. Parity and mod-4 facts for ∑ q^i come from short inductions with Nat.pow_mod and omega.