Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem #14411

Open
wants to merge 17 commits into
base: master
Choose a base branch
from
+410 −0
Open

feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem #14411

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
24d4c1c
add Order.lean
haitian-yuki May 15, 2024
1cc2784
fixes for newer lean; add line to Mathlib.lean
m4lvin Jun 12, 2024
ed84429
try to appease linter and avoid some aesops
m4lvin Jun 12, 2024
b027927
fix sorry
haitian-yuki Jul 1, 2024
e6c49b9
trivial lemmas removed
haitian-yuki Jul 3, 2024
d18ecfe
remove unnecessary
haitian-yuki Jul 3, 2024
38b7b48
replace TC with TransGen
haitian-yuki Jul 4, 2024
2f5a35d
correct indent
haitian-yuki Jul 4, 2024
d623962
remove few trivial lemmas
haitian-yuki Jul 4, 2024
ad5f762
Apply suggestions from code review
haitian-yuki Jul 9, 2024
6599ec3
replace if..then.. with by_cases
haitian-yuki Jul 10, 2024
9a64361
better naming
haitian-yuki Aug 7, 2024
db3c9e5
better naming
haitian-yuki Aug 7, 2024
49c2cd8
remove Order.lean
haitian-yuki Aug 8, 2024
22316b8
remove order
haitian-yuki Aug 8, 2024
1ee6972
fix sorries
haitian-yuki Oct 15, 2024
61d70ce
remove comments
haitian-yuki Oct 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2379,6 +2379,7 @@ import Mathlib.Data.Multiset.Antidiagonal
import Mathlib.Data.Multiset.Basic
import Mathlib.Data.Multiset.Bind
import Mathlib.Data.Multiset.Dedup
import Mathlib.Data.Multiset.DershowitzManna
import Mathlib.Data.Multiset.FinsetOps
import Mathlib.Data.Multiset.Fintype
import Mathlib.Data.Multiset.Fold
Expand Down
Loading
Loading