lean_workbook_plus_7339
ProvedFind and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7339 (n : ℕ) : ∃ u v : ℝ, u = (Real.sqrt 3 + 1) ^ (2 * n) ∧ v = (Real.sqrt 3 - 1) ^ (2 * n) := by sorry
Source
Find and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_7339 (n : ℕ) : ∃ u v : ℝ, u = (Real.sqrt 3 + 1) ^ (2 * n) ∧ v = (Real.sqrt 3 - 1) ^ (2 * n) := by sorry