mathlib3
10914620 - feat(analysis/special_functions/pow): `inv_rpow`, `div_rpow` (#2999)

Commit
5 years ago
feat(analysis/special_functions/pow): `inv_rpow`, `div_rpow` (#2999) Also use notation `ℝ≥0` and use `nnreal.eq` instead of `rw ← nnreal.coe_eq`.
Author
Parents
Loading