Theorem norm_circle_smul

Modification history

2024-08-13 09:26
Mathlib/Analysis/Complex/Circle.lean
refactor: Make `circle` a type `Circle` (#15116) …
Deleted norm_circle_smulView on Github →
2024-03-24 09:17
Mathlib/Analysis/Complex/Circle.lean
refactor(Analysis/Fourier): use `AddChar` machinery in `FourierTransform` (#11417) …
Added norm_circle_smulView on Github →