Commit 2024-05-04 05:06 1556f9eb

View on Github →

chore(Analysis/SpecialFunctions): Real.rpow -> _ ^ _ (#12613)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Log/Base.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

modified theorem tendsto_rpow_atBot_of_base_gt_one

Modified Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

modified theorem Real.continuousAt_const_rpow'

modified theorem Real.continuousAt_const_rpow

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Modified Mathlib/Topology/MetricSpace/Holder.lean