Commit 2023-03-28 10:53 f8741cbc

View on Github →

feat: port Algebra.GCDMonoid.Div (#3143)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GCDMonoid/Div.lean

added theorem Finset.Int.gcd_div_eq_one

added theorem Finset.Int.gcd_div_id_eq_one

added theorem Finset.Nat.gcd_div_eq_one

added theorem Finset.Nat.gcd_div_id_eq_one

added theorem Finset.Polynomial.gcd_div_eq_one

added theorem Finset.Polynomial.gcd_div_id_eq_one