mathlib
d36a67c7 - feat(ring_theory/euclidean_domain): generalize lemmas to PIDs (#10324)

Commit

4 years ago

feat(ring_theory/euclidean_domain): generalize lemmas to PIDs (#10324) This moves the existing lemmas to the `euclidean_domain` namespace.

Author

Ruben-VandeVelde

Parents