mathlib

2e9aa839 - chore(analysis/special_functions/pow): golf a few proofs (#8308)

chore(analysis/special_functions/pow): golf a few proofs (#8308) * add `ennreal.zero_rpow_mul_self` and `ennreal.mul_rpow_eq_ite`; * use the latter lemma to golf other proofs about `(x * y) ^ z`; * drop unneeded argument in `ennreal.inv_rpow_of_pos`, rename it to `ennreal.inv_rpow`; * add `ennreal.strict_mono_rpow_of_pos` and `ennreal.monotone_rpow_of_nonneg`, use themm to golf some proofs.