Theorem norm_circleMap_zero

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 norm_circleMap_zeroView on Github →
2025-03-25 01:16
Mathlib/Analysis/SpecialFunctions/Exp.lean
refactor(Data/Complex/Exponential): Move circleMap into Data.Complex.Exponential (#23212) …
Modified norm_circleMap_zeroView on Github →
2025-02-24 10:06
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
chore(Data/Complex): deprecate `Complex.abs` (#21995) …
Added norm_circleMap_zeroView on Github →