Commit 2025-04-18 20:13 802f7904
View on Github →chore(Algebra/GCDMonoid): generalize gcd_ne_zero_of_ lemmas (#24181)
Generalize the two lemmas gcd_ne_zero_of_left and gcd_ne_zero_of_right to not mention EuclideanDomain + GCDMonoid; they now hold for any GCD monoid.
The variable names are changed for consistency with the new surrounding lemmas.
The proofs are golfed.