lean_workbook_plus_27240
OpenSimplify to , and then turn into all sines and cosines,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27240 : 1 / Real.tan 1 = Real.cos 1 / Real.sin 1 := by sorry
Source
Simplify to , and then turn into all sines and cosines,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_27240 : 1 / Real.tan 1 = Real.cos 1 / Real.sin 1 := by sorry