Mathlib Changelog
v4
Changelog
About
Github
Theorem
injOn_circleMap_of_abs_sub_le
Modification history
2025-04-02 17:04
Mathlib/Analysis/SpecialFunctions/Complex/CircleMap.lean
feat(Analysis/SpecialFunctions/Complex/CircleMap): some basic facts about `circleMap` (#23167) …
Added
injOn_circleMap_of_abs_sub_le
View on Github →