lean_workbook_plus_9607
OpenProve that the roots of the equation are where .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9607 (x : ℝ) : sin x = 0 ↔ ∃ n : ℤ, x = n * π := by sorry
Source
Prove that the roots of the equation are where .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9607 (x : ℝ) : sin x = 0 ↔ ∃ n : ℤ, x = n * π := by sorry