Commit 2023-05-15 19:52 0b9eaaa7

chore(analysis/special_functions): split up pow.lean (#19006) This PR splits up the monster file analysis.special_functions.pow into the following 6 files:

• pow_complex: definition of a ^ b for complex a, b and basic properties (179 lines)
• pow_real: definition of a ^ b for real a, b & lemmas about order / monotonicity (641 lines)
• pow_nnreal: definitions for nnreal and ennreal types (693 lines)
• pow_asymptotics: limiting behaviour at infinity (282 lines)
• pow_continuity: continuity properties (500 lines)
• pow_tactic: extensions to positivity and norm_num for powers (209 lines) No code has been added or removed, only moved around, and the only changes outside these files are adjustments to imports.