ENNReal.rpow_ofNNReal

Stream: Is there code for X?

[Michael Rothgang]

I have one sorry in branch#MR-generalise-enorm-6 which would be closed by the following statement. Is this really missing from mathlib?

theorem ENNReal.rpow_ofNNReal {M : ℝ≥0} {P : ℝ} :
  (ENNReal.ofNNReal M).rpow P = ENNReal.ofNNReal (M ^ P) := sorry

[Ruben Van de Velde]

import Mathlib
open NNReal
theorem ENNReal.rpow_ofNNReal {M : ℝ≥0} {P : ℝ} :
    (ENNReal.ofNNReal M) ^ P = ENNReal.ofNNReal (M ^ P) := by
  rw [coe_rpow_def]
  -- ⊢ (if M = 0 ∧ P < 0 then ⊤ else ↑(M ^ P)) = ↑(M ^ P)

Seems like it's false

[Andrew Yang]

docs#ENNReal.coe_rpow_of_nonneg

[Yaël Dillies]

.. which btw is the wrong way around

[Michael Rothgang]

If you submit a PR renaming it, I'll happily review it.