lean_workbook_plus_34171
OpenGiven , prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34171 : ∀ C : ℝ, sin C * (1 - sin C) ≤ 1 / 4 := by sorry
Source
Given , prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_34171 : ∀ C : ℝ, sin C * (1 - sin C) ≤ 1 / 4 := by sorry