Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.sqrt_lt'

Modification history

2022-04-20 18:42
src/data/real/sqrt.lean
feat(data/real/sqrt): `sqrt x < y ↔ x < y^2` (#13546) …
Added real.sqrt_lt'View on Github →