Sine_and_Cosine_are_Periodic_on_Reals

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysisperiodicityproofwikitrigonometry

cos(x + 2pi) = cos(x) and sin(x + 2pi) = sin(x) for all real x.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

theorem Sine_and_Cosine_are_Periodic_on_Reals (x : ℝ) : Real.cos (x + 2 * Real.pi) = Real.cos x ∧ Real.sin (x + 2 * Real.pi) = Real.sin x := by sorry

Source

https://proofwiki.org/wiki/Sine_and_Cosine_are_Periodic_on_Reals

View graph