feat: port Analysis.SpecialFunctions.Complex.Arg (#4041)

leanprover-community · May 18, 2023 · 5a1d44a · 5a1d44a
1 parent 01d72c4
commit 5a1d44a
Show file tree

Hide file tree

Showing 2 changed files with 635 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -434,6 +434,7 @@ import Mathlib.Analysis.NormedSpace.RieszLemma
 import Mathlib.Analysis.NormedSpace.Star.Basic
 import Mathlib.Analysis.NormedSpace.Units
 import Mathlib.Analysis.Seminorm
+import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Analysis.SpecialFunctions.Polynomials