Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-20 07:52 8d40e8d0

View on Github →

feat(analysis/special_functions/pow): add ennreal.to_nnreal_rpow (#5042) cut ennreal.to_real_rpow into two lemmas: to_nnreal_rpow and to_real_rpow

Estimated changes

added theorem ennreal.to_nnreal_rpow
modified theorem ennreal.to_real_rpow