Commit 2020-09-28 05:25 66c87c0d
View on Github →feat(data/*/gcd): adds gcd, lcm of finsets and multisets (#4217)
Defines finset.gcd
, finset.lcm
, multiset.gcd
, multiset.lcm
Proves some basic facts about those, analogous to those in data.multiset.lattice
and data.finset.lattice