GCD and LCM operations on finsets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
Implementation notes #
Many of the proofs use the lemmas
lcm.def, which relate
TODO: simplify with a tactic and
Least common multiple of a finite set
Greatest common divisor of a finite set