Commit 2025-11-21 13:53 4016936e
View on Github →chore(RingTheory): generalize to Nonempty NormalizedGCDMonoid in GaussLemma (#31874)
because there is an instance from UniqueFactorizationMonoid to Nonempty NormalizedGCDMonoid but not to NormalizedGCDMonoid.