Commit 2023-06-15 15:45 bf9bbbcf

View on Github →

feat(field_theory/ratfunc): The numerator and denominator of a rational function are coprime (#18652) Also make more arguments to gcd_ne_zero_of_left/gcd_ne_zero_of_right implicit.

Estimated changes

Modified src/algebra/euclidean_domain/basic.lean

Modified src/field_theory/ratfunc.lean

added theorem ratfunc.is_coprime_num_denom

Modified src/ring_theory/euclidean_domain.lean

modified theorem gcd_ne_zero_of_left

modified theorem gcd_ne_zero_of_right

added theorem is_coprime_div_gcd_div_gcd