lean_workbook_plus_75190
OpenUse the trigonometric identity \n
to rewrite the expression.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75190 (x : ℝ) : tan (π/2 - x) = 1 / tan x := by sorry
Source
Use the trigonometric identity \n
to rewrite the expression.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_75190 (x : ℝ) : tan (π/2 - x) = 1 / tan x := by sorry