Commit 2023-01-16 21:23 65e2763c

View on Github →

feat: port Algebra.GCDMonoid.Multiset (#1565)

Estimated changes

added theorem Multiset.dvd_gcd
added theorem Multiset.dvd_lcm
added theorem Multiset.extract_gcd'
added theorem Multiset.extract_gcd
added def Multiset.gcd
added theorem Multiset.gcd_add
added theorem Multiset.gcd_cons
added theorem Multiset.gcd_dedup
added theorem Multiset.gcd_dvd
added theorem Multiset.gcd_map_mul
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_dedup
added theorem Multiset.lcm_dvd
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