lean_workbook_plus_27783
OpenFind the solutions to the equation .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27783 : ∀ x : ℝ, sin (7 * x) = 0 ↔ ∃ k : ℤ, x = k * π / 7 := by sorry
Source
Find the solutions to the equation .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_27783 : ∀ x : ℝ, sin (7 * x) = 0 ↔ ∃ k : ℤ, x = k * π / 7 := by sorry