Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

added theorem finset.dvd_gcd
added theorem finset.dvd_gcd_iff
added theorem finset.dvd_lcm
added def finset.gcd
added theorem finset.gcd_congr
added theorem finset.gcd_def
added theorem finset.gcd_dvd
added theorem finset.gcd_empty
added theorem finset.gcd_insert
added theorem finset.gcd_mono
added theorem finset.gcd_mono_fun
added theorem finset.gcd_singleton
added theorem finset.gcd_union
added def finset.lcm
added theorem finset.lcm_congr
added theorem finset.lcm_def
added theorem finset.lcm_dvd
added theorem finset.lcm_dvd_iff
added theorem finset.lcm_empty
added theorem finset.lcm_insert
added theorem finset.lcm_mono
added theorem finset.lcm_mono_fun
added theorem finset.lcm_singleton
added theorem finset.lcm_union
added theorem finset.normalize_gcd
added theorem finset.normalize_lcm
added theorem multiset.dvd_gcd
added theorem multiset.dvd_lcm
added def multiset.gcd
added theorem multiset.gcd_add
added theorem multiset.gcd_cons
added theorem multiset.gcd_dvd
added theorem multiset.gcd_erase_dup
added theorem multiset.gcd_mono
added theorem multiset.gcd_ndinsert
added theorem multiset.gcd_ndunion
added theorem multiset.gcd_singleton
added theorem multiset.gcd_union
added theorem multiset.gcd_zero
added def multiset.lcm
added theorem multiset.lcm_add
added theorem multiset.lcm_cons
added theorem multiset.lcm_dvd
added theorem multiset.lcm_erase_dup
added theorem multiset.lcm_mono
added theorem multiset.lcm_ndinsert
added theorem multiset.lcm_ndunion
added theorem multiset.lcm_singleton
added theorem multiset.lcm_union
added theorem multiset.lcm_zero
added theorem multiset.normalize_gcd
added theorem multiset.normalize_lcm