Theorem gcd_ne_zero_of_left

Modification history

2025-04-18 20:13
Mathlib/Algebra/GCDMonoid/Basic.lean
chore(Algebra/GCDMonoid): generalize gcd_ne_zero_of_ lemmas (#24181) …
Modified gcd_ne_zero_of_leftView on Github →
2023-06-19 09:13
Mathlib/RingTheory/EuclideanDomain.lean
feat: The numerator and denominator of a rational function are coprime (#5136) …
Modified gcd_ne_zero_of_leftView on Github →
2023-03-21 13:27
Mathlib/RingTheory/EuclideanDomain.lean
feat: port RingTheory.EuclideanDomain (#3017)
Added gcd_ne_zero_of_leftView on Github →