Theorem Complex.circleMap_neg_pi_div_two

Modification history

2025-04-02 17:04
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
feat(Analysis/SpecialFunctions/Complex/CircleMap): some basic facts about `circleMap` (#23167) …
Deleted Complex.circleMap_neg_pi_div_twoView on Github →
2025-03-26 20:16
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
feature(Analysis/SpecialFunctions/Trigonometric/Basic): basic facts about complex numbers (#23165) …
Added Complex.circleMap_neg_pi_div_twoView on Github →