mathlib3
8d40e8d0
- feat(analysis/special_functions/pow): add ennreal.to_nnreal_rpow (#5042)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
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
Author
RemyDegenne
Parents
de76acdc
Loading