Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-16 07:20 20fe4a16

View on Github →

feat(algebra/euclidean_domain): some cleanup (#3752) Lower the priority of simp-lemmas which have an equivalent version in group_with_zero, so that the version of group_with_zero is found by squeeze_simp for types that have both structures. Add docstrings Remove outdated comment

Estimated changes