mathlib

6e64492d - feat(ring_theory/multiplicity): Equality of `factorization`, `multiplicity`, and `padic_val_nat` (#12033)

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`.