Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-20 18:42 27a8328b

View on Github →

feat(data/real/sqrt): sqrt x < y ↔ x < y^2 (#13546) Prove real.sqrt_lt_iff and generalize real.lt_sqrt.

Estimated changes

modified theorem real.le_sqrt'
modified theorem real.lt_sqrt
modified theorem real.sq_lt
added theorem real.sqrt_lt'
added theorem real.sqrt_lt