Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-29 01:02 e63a4d5e

View on Github →

feat(analysis/special_functions/pow): sqrt and inequalities (#16515) This PR proves a few lemmas about real.sqrt and real.rpow as well as inequality lemmas for negative powers.

Estimated changes