feat: port Data.Finset.Image (#1586)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
leanprover-community · Jan 16, 2023 · fa90299 · fa90299
1 parent 09a26db
commit fa90299
Show file tree

Hide file tree

Showing 3 changed files with 806 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -223,6 +223,7 @@ import Mathlib.Data.Fin.Fin2
 import Mathlib.Data.Fin.SuccPred
 import Mathlib.Data.Finite.Defs
 import Mathlib.Data.Finset.Basic
+import Mathlib.Data.Finset.Image
 import Mathlib.Data.Finset.Order
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.FunLike.Basic