mathlib3

739e831f - feat(analysis/complex/exponential): real powers of nnreals (#2164)

feat(analysis/complex/exponential): real powers of nnreals (#2164) * feat(analysis/complex/exponential): real powers of nnreals * cleanup * mean inequalities in nnreal * mean inequalities * use < instead of > * reviewer's comments Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>