Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-26 15:49 8e838058

View on Github →

chore(analysis/special_functions/pow): +2 lemmas about nnreal.rpow (#4272) λ x, x^y is continuous in more cases than λ p, p.1^p.2.

Estimated changes