mathlib

0830c456 - feat(algebra/gcd_monoid/finset): Generalize `finset.gcd_image` (#16795)

feat(algebra/gcd_monoid/finset): Generalize `finset.gcd_image` (#16795) `finset.gcd_image` and `finset.gcd_eq_gcd_image` were unnecessarily assuming `[is_idempotent α gcd]`. Remove that assumption and add the corresponding `finset.lcm` lemmas.