Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-22 14:56 56bedb40

View on Github →

feat(analysis/special_functions/exp_log): continuous_on_exp/pow (#7243)

Estimated changes

Modified src/analysis/special_functions/exp_log.lean

added theorem complex.continuous_on_exp

added theorem real.continuous_on_exp

Modified src/analysis/special_functions/integrals.lean

Modified src/topology/algebra/monoid.lean

added theorem continuous_on_pow