lean_workbook_plus_41487
ProvedAssume that and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_41487 : ∃ x : ℕ → ℝ, x 2 = 0 ∧ x 3 = 0 ∧ x 2015 = 0 ∧ x 1 = 1 := by sorry
Source
Assume that and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_41487 : ∃ x : ℕ → ℝ, x 2 = 0 ∧ x 3 = 0 ∧ x 2015 = 0 ∧ x 1 = 1 := by sorry