Commit 2026-03-20 14:17 65212201

chore(Data/Nat/Factorization/Defs): rename factorization_prod_pow_eq_self to prod_factorization_pow_eq_self (#36842) The statement is n.factorization.prod (· ^ ·) = n, and without dot notation it is Finsupp.prod (Nat.factorization n) (· ^ ·) = n, therefore the order should be prod then factorization then pow. Not to be confused with prod_pow_factorization_eq_self: Its statement is (f.prod (· ^ ·)).factorization = f, and without dot notation it is Nat.factorization (Finsupp.prod f (· ^ ·)) = f, therefore it should be the one named factorization_prod_pow_eq_self. This will have to wait for the current rename.