lean_workbook_plus_43022
ProvedFind given that is a real root of the equation .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43022 (a : ℝ) (ha : a^5 - a^3 + a - 2 = 0) : ⌊a^6⌋ = 3 := by sorry
Source
Find given that is a real root of the equation .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_43022 (a : ℝ) (ha : a^5 - a^3 + a - 2 = 0) : ⌊a^6⌋ = 3 := by sorry