lean_workbook_plus_9408
OpenSolve: with and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9408 (x : ℝ) (hx : x > 0 ∧ x ≠ 1) : x^((Real.log 30) / (Real.log x)) = 30 := by sorry
Source
Solve: with and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9408 (x : ℝ) (hx : x > 0 ∧ x ≠ 1) : x^((Real.log 30) / (Real.log x)) = 30 := by sorry