feat: port Mathlib.Data.List.Sigma (#1493)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
leanprover-community · Jan 13, 2023 · 64e7042 · 64e7042
1 parent 90f9001
commit 64e7042
Show file tree

Hide file tree

Showing 2 changed files with 798 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -278,6 +278,7 @@ import Mathlib.Data.List.ProdSigma
 import Mathlib.Data.List.Range
 import Mathlib.Data.List.Rdrop
 import Mathlib.Data.List.Sections
+import Mathlib.Data.List.Sigma
 import Mathlib.Data.List.TFAE
 import Mathlib.Data.List.Zip
 import Mathlib.Data.Multiset.Basic