lean_workbook_plus_48665
OpenExplain why if , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48665 (x z : ℝ) : Real.logb 2 x = z → Real.logb x 2 = 1 / z := by sorry
Source
Explain why if , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_48665 (x z : ℝ) : Real.logb 2 x = z → Real.logb x 2 = 1 / z := by sorry