lean_workbook_plus_8562
OpenProve that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8562 (a x y : ℝ) (ha : 0 < a) : a^x * a^y = a^(x + y) := by sorry
Source
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_8562 (a x y : ℝ) (ha : 0 < a) : a^x * a^y = a^(x + y) := by sorry