Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.lt_sq_of_sqrt_lt

Modification history

2022-07-11 08:26
src/data/real/sqrt.lean
feat(analysis/special_functions/pow): Rational powers are dense (#15002) …
Added real.lt_sq_of_sqrt_ltView on Github →