Skip to content

Commit a687226

Browse files
committed
chore(SpecialFunctions/Log): fix naming typo (leanprover-community#41773)
This lemma used to be named `EReal.ENNReal.rpow_eq_exp_mul_log` which I presume was accidental and the name was intended to be `ENNReal.rpow_eq_exp_mul_log`, and so this PR renames accordingly.
1 parent ecc9242 commit a687226

1 file changed

Lines changed: 7 additions & 3 deletions

File tree

Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -63,13 +63,17 @@ lemma exp_nmul (x : EReal) (n : ℕ) : exp (n * x) = (exp x) ^ n := by
6363
lemma exp_mul (x : EReal) (y : ℝ) : exp (x * y) = (exp x) ^ y := by
6464
rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]
6565

66-
lemma ENNReal.rpow_eq_exp_mul_log (x : ℝ≥0∞) (y : ℝ) : x ^ y = exp (y * log x) := by
67-
rw [mul_comm, EReal.exp_mul, exp_log]
68-
6966
end EReal
7067
end Exp
7168

7269
namespace ENNReal
70+
71+
lemma rpow_eq_exp_mul_log (x : ℝ≥0∞) (y : ℝ) : x ^ y = exp (y * log x) := by
72+
rw [← log_rpow, exp_log]
73+
74+
@[deprecated (since := "2026-07-15")] alias _root_.EReal.ENNReal.rpow_eq_exp_mul_log :=
75+
rpow_eq_exp_mul_log
76+
7377
section OrderIso
7478

7579
set_option backward.isDefEq.respectTransparency false in

0 commit comments

Comments
 (0)