x^y=z from y.log(x)=log(z)

Stream: Is there code for X?

[Kevin Buzzard]

Do we really not have this:

import Mathlib

open Real

example (x y z : ℝ) (hx : 0 < x) (hz : 0 < z) (h : y * log x = log z) : x ^ y = z := sorry

Did I slip up somewhere?

[Kevin Buzzard]

import Mathlib

open Real

example (x y z : ℝ) (hx : 0 < x) (hz : 0 < z) (h : y * log x = log z) : x ^ y = z := by
  rw [← log_rpow hx] at h
  apply_fun Real.exp at h
  rwa [exp_log, exp_log hz] at h
  apply rpow_pos_of_pos hx

[Kevin Buzzard]

#6469

[Eric Wieser]

example (x y z : ℝ) (hx : 0 < x) (hz : 0 < z) (h : y * log x = log z) : x ^ y = z :=
  log_injOn_pos (rpow_pos_of_pos hx _) hz <| log_rpow hx _ |>.trans h

[Eric Wieser]

While we're on the subject of rpow, #6470 adds some nearby missing lemmas