lean_workbook_plus_44985
OpenProve that using power series definitions of sine and cosine.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44985 (x : ℝ) : |sin x| ≤ 1 := by sorry
Source
Prove that using power series definitions of sine and cosine.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_44985 (x : ℝ) : |sin x| ≤ 1 := by sorry