Commit 2024-07-14 02:03 670cd521

feat(SpecialFunctions.Log.ENNRealLog): remove a coercion in log_pow (#14714) The previous version of the lemma stated that log (x ^ n) = (n : ℝ≥0∞) * log x. Changed to log (x ^ n) = n * log x, removing a coercion. There are many different coercions from Nat, Real, etc. to EReal. I think statements should as much as possible use the "canonical" coercion, which from Nat to EReal is the AddMonoidWithOne coercion. Anything more complicated (here, going from Nat -> ENNReal -> EReal) gets quickly into coercion hell.