Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-03 20:33 c0f7c56e

View on Github →

feat(algebra/order): exists_square_le (#9513) This is a modernized version of code from the perfectoid project.

Estimated changes