Commit 2023-01-17 08:44 98d34d74

View on Github →

feat: port Algebra.GCDMonoid.Finset (#1612)

Estimated changes

added theorem Finset.dvd_gcd
added theorem Finset.dvd_gcd_iff
added theorem Finset.dvd_lcm
added theorem Finset.extract_gcd'
added theorem Finset.extract_gcd
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_eq_zero_iff
added theorem Finset.gcd_image
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_eq_zero_iff
added theorem Finset.lcm_image
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