mathlib
66c87c0d - feat(data/*/gcd): adds gcd, lcm of finsets and multisets (#4217)

Commit
5 years ago
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` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Author
Parents
Loading