Commit 2022-02-15 15:52 6e64492d
View on Github →feat(ring_theory/multiplicity): Equality of factorization, multiplicity, and padic_val_nat (#12033)
Proves multiplicity_eq_factorization : multiplicity p n = n.factorization p for prime p and n ≠ 0 and uses this to golf the proof of padic_val_nat_eq_factorization : padic_val_nat p n = n.factorization p.