Def circleMap

Modification history

2025-04-02 17:04

Mathlib/Analysis/SpecialFunctions/Complex/CircleMap.lean

feat(Analysis/SpecialFunctions/Complex/CircleMap): some basic facts about `circleMap` (#23167) …

Modified circleMap View on Github →

2025-03-25 01:16

Mathlib/Data/Complex/Exponential.lean

refactor(Data/Complex/Exponential): Move circleMap into Data.Complex.Exponential (#23212) …

Modified circleMap View on Github →

2023-06-09 02:13

Mathlib/MeasureTheory/Integral/CircleIntegral.lean

feat: port MeasureTheory.Integral.CircleIntegral (#4858)

Added circleMap View on Github →