feat: port Data.Setoid.Basic (#1117)

Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
leanprover-community · Dec 22, 2022 · 7374a9a · 7374a9a
1 parent afe3592
commit 7374a9a
Show file tree

Hide file tree

Showing 2 changed files with 486 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -266,6 +266,7 @@ import Mathlib.Data.Set.Opposite
 import Mathlib.Data.Set.Prod
 import Mathlib.Data.Set.Sigma
 import Mathlib.Data.SetLike.Basic
+import Mathlib.Data.Setoid.Basic
 import Mathlib.Data.Sigma.Basic
 import Mathlib.Data.Sigma.Lex
 import Mathlib.Data.Sigma.Order