mathlib
0b9eaaa7 - chore(analysis/special_functions): split up `pow.lean` (#19006)

Commit
2 years ago
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.
Author
Parents
Loading