Commit 2021-07-14 11:55 2e9aa839

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.