Theorem Real.sin_eq_one_iff

Modification history

2024-01-25 13:08
Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
feat(Trigonometric): add lemmas about `cos x = -1 ↔ _` etc (#9878)
Added Real.sin_eq_one_iffView on Github →