Theorem Circle.exp_surjective

Modification history

2026-04-14 17:36

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

feat(Analysis/SpecialFunctions/Complex/Circle): `Circle.exp` is `InjOn` intervals shorter than 2π (#37813) …

Added Circle.exp_surjective View on Github →