mathlib
c0f7c56e - feat(algebra/order): exists_square_le (#9513)

Commit

4 years ago

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

Author

PatrickMassot

Parents