Commit 2024-01-25 13:08 ce79848a

View on Github →

feat(Trigonometric): add lemmas about cos x = -1 ↔ _ etc (#9878)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean

added theorem Complex.cos_eq_neg_one_iff

added theorem Complex.cos_eq_one_iff

added theorem Complex.sin_eq_neg_one_iff

added theorem Complex.sin_eq_one_iff

added theorem Real.cos_eq_neg_one_iff

modified theorem Real.cos_ne_zero_iff

added theorem Real.sin_eq_neg_one_iff

added theorem Real.sin_eq_one_iff