mathlib3

43cd4142 - feat(algebra/gcd_monoid): extract gcd from multiset/finset (#17316)

feat(algebra/gcd_monoid): extract gcd from multiset/finset (#17316) + `multiset.extract_gcd` / `finset.extract_gcd`: extract the gcd as a common factor from a nonempty multiset/finset in a `normalized_gcd_monoid`, so that the gcd of remaining factors is 1. + We prove these by induction, which require the more precise version of the two-element case `_root_.extract_gcd` with `d := gcd a b`. inspired by #16838 Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>