mathlib

597343b0 - feat(ring_theory): induction and multiplicativity via prime factorization (#17192)

feat(ring_theory): induction and multiplicativity via prime factorization (#17192) Two pairs of lemmas for unique factorization domains, where we can show that a property holds on all elements, or a function is multiplicative, by showing this works on base cases, products of coprime elements and powers of prime elements. We will use the last result to show the ideal norm is a multiplicative map. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>