Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-17 08:44
98d34d74
View on Github →
feat: port Algebra.GCDMonoid.Finset (
#1612
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/GCDMonoid/Finset.lean
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_gcd_filter_ne_zero
added
theorem
Finset.gcd_eq_gcd_image
added
theorem
Finset.gcd_eq_of_dvd_sub
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_lcm_image
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