Mathlib v3 is deprecated. Go to Mathlib v4

Theorem gcd_ne_zero_of_left

Modification history

2023-06-15 15:45
src/ring_theory/euclidean_domain.lean
feat(field_theory/ratfunc): The numerator and denominator of a rational function are coprime (#18652) …
Modified gcd_ne_zero_of_leftView on Github →
2022-01-30 00:12
src/ring_theory/euclidean_domain.lean
feat(field_theory/ratfunc): rational functions as Laurent series (#11276)
Added gcd_ne_zero_of_leftView on Github →