lean_workbook_plus_38005
Provedor
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38005 (t : ℝ) : (t^2 = 1/3) ↔ t = 1/Real.sqrt 3 ∨ t = -1/Real.sqrt 3 := by sorry
Source
or
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_38005 (t : ℝ) : (t^2 = 1/3) ↔ t = 1/Real.sqrt 3 ∨ t = -1/Real.sqrt 3 := by sorry