mathlib

d33792e6 - feat(data/nat/factorization): add lemma `factorization_gcd` (#11605)

feat(data/nat/factorization): add lemma `factorization_gcd` (#11605) For positive `a` and `b`, `(gcd a b).factorization = a.factorization ⊓ b.factorization`; i.e. the power of prime `p` in `gcd a b` is the minimum of its powers in `a` and `b`. This is Theorem 1.12 in Apostol (1976) Introduction to Analytic Number Theory.