feat: port Data.Complex.Basic (#2718)

leanprover-community · Mar 10, 2023 · a79a9dc · a79a9dc
1 parent 055fd87
commit a79a9dc
Show file tree

Hide file tree

Showing 2 changed files with 1,374 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -469,6 +469,7 @@ import Mathlib.Data.Bracket
 import Mathlib.Data.Bundle
 import Mathlib.Data.ByteArray
 import Mathlib.Data.Char
+import Mathlib.Data.Complex.Basic
 import Mathlib.Data.Countable.Basic
 import Mathlib.Data.Countable.Defs
 import Mathlib.Data.Countable.Small