Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.angle.cos_eq_iff_coe_eq_or_eq_neg

Modification history

2022-07-27 17:03

src/analysis/special_functions/trigonometric/angle.lean

feat(analysis/special_functions/trigonometric/angle): equality of `cos` or `sin` (#15651) …

Added real.angle.cos_eq_iff_coe_eq_or_eq_neg View on Github →