Commit 2023-06-19 09:13 118d7129

View on Github →

feat: The numerator and denominator of a rational function are coprime (#5136) Match https://github.com/leanprover-community/mathlib/pull/18652

Estimated changes

Modified Mathlib/Algebra/EuclideanDomain/Basic.lean

Modified Mathlib/FieldTheory/RatFunc.lean

added theorem RatFunc.isCoprime_num_denom

Modified Mathlib/RingTheory/EuclideanDomain.lean

modified theorem gcd_ne_zero_of_left

modified theorem gcd_ne_zero_of_right

added theorem isCoprime_div_gcd_div_gcd