Skip to content

Commit

Permalink
feat: Port Data.Set.Image (#949)
Browse files Browse the repository at this point in the history
mathlib3 SHA: f178c0e25af359f6cbc72a96a243efd3b12423a3

- [x] depends on: #892

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Co-authored-by: Winston Yin <winstonyin@gmail.com>
  • Loading branch information
4 people committed Dec 12, 2022
1 parent d29c2cb commit a6ba4bb
Show file tree
Hide file tree
Showing 2 changed files with 1,543 additions and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Expand Up @@ -180,6 +180,7 @@ import Mathlib.Data.Rat.Defs
import Mathlib.Data.Rat.Init
import Mathlib.Data.Rat.Order
import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Image
import Mathlib.Data.Sigma.Basic
import Mathlib.Data.Sigma.Lex
import Mathlib.Data.Sigma.Order
Expand Down

0 comments on commit a6ba4bb

Please sign in to comment.