-
Notifications
You must be signed in to change notification settings - Fork 238
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.
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
chore: changes to adapt to leanprover/lean4#2644 #7606
Closed
Closed
Changes from 1 commit
Commits
Show all changes
499 commits
Select commit
Hold shift + click to select a range
e8db259
Merge master into nightly-testing
leanprover-community-mathlib4-bot cd97f2e
Merge master into nightly-testing
leanprover-community-mathlib4-bot f02fdbf
Merge master into nightly-testing
leanprover-community-mathlib4-bot 19805f6
Merge master into nightly-testing
leanprover-community-mathlib4-bot ef0e7c1
Merge master into nightly-testing
leanprover-community-mathlib4-bot eafc575
Merge master into nightly-testing
leanprover-community-mathlib4-bot 2f03cc8
Merge master into nightly-testing
leanprover-community-mathlib4-bot 17a4465
Merge master into nightly-testing
leanprover-community-mathlib4-bot 10edb20
Merge master into nightly-testing
leanprover-community-mathlib4-bot fdd6434
chore: bump to nightly-2023-09-20
leanprover-community-mathlib4-bot 488b427
Merge master into nightly-testing
leanprover-community-mathlib4-bot 5f8dfc3
Merge master into nightly-testing
leanprover-community-mathlib4-bot 4048ff9
Merge master into nightly-testing
leanprover-community-mathlib4-bot 64af06e
Merge master into nightly-testing
leanprover-community-mathlib4-bot 7aff542
Merge master into nightly-testing
leanprover-community-mathlib4-bot 450d567
Merge master into nightly-testing
leanprover-community-mathlib4-bot da34301
Trigger CI for https://github.com/leanprover/lean4/pull/2502
leanprover-community-mathlib4-bot 7a80ae7
Merge master into nightly-testing
leanprover-community-mathlib4-bot f3cdca8
Merge master into nightly-testing
leanprover-community-mathlib4-bot fcc8232
Merge master into nightly-testing
leanprover-community-mathlib4-bot 92542a8
chore: bump to nightly-2023-09-21
leanprover-community-mathlib4-bot 5e79e76
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6bbc802
Merge master into nightly-testing
leanprover-community-mathlib4-bot 73e8d32
Merge master into nightly-testing
leanprover-community-mathlib4-bot 26d7ca2
Merge master into nightly-testing
leanprover-community-mathlib4-bot 363e810
Merge master into nightly-testing
leanprover-community-mathlib4-bot f3f41ea
Merge master into nightly-testing
leanprover-community-mathlib4-bot b534ed4
Merge master into nightly-testing
leanprover-community-mathlib4-bot 0ad2194
Merge master into nightly-testing
leanprover-community-mathlib4-bot 105030f
Merge master into nightly-testing
leanprover-community-mathlib4-bot 0c87732
Merge master into nightly-testing
leanprover-community-mathlib4-bot 02e4bee
Merge master into nightly-testing
leanprover-community-mathlib4-bot 121ae13
Merge master into nightly-testing
leanprover-community-mathlib4-bot 46cd885
merge
semorrison 3043876
Merge branch 'nightly-testing' of github.com:leanprover-community/mat…
semorrison 35d45df
Merge master into nightly-testing
leanprover-community-mathlib4-bot d823d83
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6e44d98
Merge master into nightly-testing
leanprover-community-mathlib4-bot b3c2a59
Merge master into nightly-testing
leanprover-community-mathlib4-bot 659605e
Merge master into nightly-testing
leanprover-community-mathlib4-bot aca6bf5
Merge master into nightly-testing
leanprover-community-mathlib4-bot a56cd1f
chore: bump to nightly-2023-09-22
leanprover-community-mathlib4-bot caa1b98
Merge master into nightly-testing
leanprover-community-mathlib4-bot 151bf91
Merge master into nightly-testing
leanprover-community-mathlib4-bot c19fb6a
Merge master into nightly-testing
leanprover-community-mathlib4-bot 087eb61
Merge master into nightly-testing
leanprover-community-mathlib4-bot 57be952
Merge master into nightly-testing
leanprover-community-mathlib4-bot 87b0303
Merge master into nightly-testing
leanprover-community-mathlib4-bot 98c132a
Merge master into nightly-testing
leanprover-community-mathlib4-bot 9c0f022
Merge master into nightly-testing
leanprover-community-mathlib4-bot 1efa4bb
chore: bump to nightly-2023-09-23
leanprover-community-mathlib4-bot 8352a04
Merge master into nightly-testing
leanprover-community-mathlib4-bot fe44ffb
Merge master into nightly-testing
leanprover-community-mathlib4-bot 0d1a58e
Merge master into nightly-testing
leanprover-community-mathlib4-bot 8262ccb
Merge master into nightly-testing
leanprover-community-mathlib4-bot ee03a68
Merge master into nightly-testing
leanprover-community-mathlib4-bot a5c27ad
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6b3a65b
Merge master into nightly-testing
leanprover-community-mathlib4-bot a477df9
Merge master into nightly-testing
leanprover-community-mathlib4-bot 0a07e84
Merge master into nightly-testing
leanprover-community-mathlib4-bot c4bc5ee
Merge master into nightly-testing
leanprover-community-mathlib4-bot f0b5dae
Merge master into nightly-testing
leanprover-community-mathlib4-bot 0c3215e
Merge master into nightly-testing
leanprover-community-mathlib4-bot d3760a1
Merge master into nightly-testing
leanprover-community-mathlib4-bot 5beacf7
Merge master into nightly-testing
leanprover-community-mathlib4-bot 3665a74
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6278b14
Merge master into nightly-testing
leanprover-community-mathlib4-bot 7f30787
Merge master into nightly-testing
leanprover-community-mathlib4-bot f9dc45b
chore: bump to nightly-2023-09-26
leanprover-community-mathlib4-bot 83ced17
Merge master into nightly-testing
leanprover-community-mathlib4-bot 794aae9
Merge master into nightly-testing
leanprover-community-mathlib4-bot 52747e6
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6d9eb92
Merge master into nightly-testing
leanprover-community-mathlib4-bot 3c707e7
Merge master into nightly-testing
leanprover-community-mathlib4-bot 62b963e
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6185e0c
Merge master into nightly-testing
leanprover-community-mathlib4-bot 8914f4b
Merge master into nightly-testing
leanprover-community-mathlib4-bot 5a79c9c
Merge master into nightly-testing
leanprover-community-mathlib4-bot 815f5bd
Merge master into nightly-testing
leanprover-community-mathlib4-bot 11d7489
Merge master into nightly-testing
leanprover-community-mathlib4-bot 135efb2
Merge master into nightly-testing
leanprover-community-mathlib4-bot 0d10fe3
chore: bump to nightly-2023-09-27
leanprover-community-mathlib4-bot 49d4d99
Merge master into nightly-testing
leanprover-community-mathlib4-bot d555c7f
Merge master into nightly-testing
leanprover-community-mathlib4-bot 333de50
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6d33e0c
Merge master into nightly-testing
leanprover-community-mathlib4-bot 90bd5df
Merge master into nightly-testing
leanprover-community-mathlib4-bot 7b24469
Merge master into nightly-testing
leanprover-community-mathlib4-bot cc52df8
Merge master into nightly-testing
leanprover-community-mathlib4-bot 73e3896
Merge master into nightly-testing
leanprover-community-mathlib4-bot cdc40bc
Merge master into nightly-testing
leanprover-community-mathlib4-bot 60b6532
chore: bump to nightly-2023-09-28
leanprover-community-mathlib4-bot 64d04c7
Merge master into nightly-testing
leanprover-community-mathlib4-bot ce20f2d
Merge master into nightly-testing
leanprover-community-mathlib4-bot c9d73cc
Merge master into nightly-testing
leanprover-community-mathlib4-bot 4ff1b1f
Merge master into nightly-testing
leanprover-community-mathlib4-bot 0015bc2
Merge master into nightly-testing
leanprover-community-mathlib4-bot cec4a39
Merge master into nightly-testing
leanprover-community-mathlib4-bot f5c91dd
Merge master into nightly-testing
leanprover-community-mathlib4-bot 351d3ed
Merge master into nightly-testing
leanprover-community-mathlib4-bot cbe1a8d
Merge master into nightly-testing
leanprover-community-mathlib4-bot f9bafbe
Merge master into nightly-testing
leanprover-community-mathlib4-bot 4895ca1
Merge master into nightly-testing
leanprover-community-mathlib4-bot fd61c53
Merge master into nightly-testing
leanprover-community-mathlib4-bot 82f7788
Merge master into nightly-testing
leanprover-community-mathlib4-bot ef42224
Merge master into nightly-testing
leanprover-community-mathlib4-bot a419b72
Merge master into nightly-testing
leanprover-community-mathlib4-bot 466c100
Merge master into nightly-testing
leanprover-community-mathlib4-bot ee39108
Merge master into nightly-testing
leanprover-community-mathlib4-bot d030098
chore: bump to nightly-2023-10-01
leanprover-community-mathlib4-bot 3dd6cef
Merge master into nightly-testing
leanprover-community-mathlib4-bot c411c7c
Merge master into nightly-testing
leanprover-community-mathlib4-bot ec286d5
Merge master into nightly-testing
leanprover-community-mathlib4-bot 4118518
Merge master into nightly-testing
leanprover-community-mathlib4-bot 320dd25
Merge master into nightly-testing
leanprover-community-mathlib4-bot e6d2325
Merge master into nightly-testing
leanprover-community-mathlib4-bot 1139f8d
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6deb700
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6bbc345
Merge master into nightly-testing
leanprover-community-mathlib4-bot ef071fd
Merge master into nightly-testing
leanprover-community-mathlib4-bot 3f9d324
Merge master into nightly-testing
leanprover-community-mathlib4-bot 4b76ea4
Merge master into nightly-testing
leanprover-community-mathlib4-bot 5f86892
Merge master into nightly-testing
leanprover-community-mathlib4-bot 247e3c0
chore: bump to nightly-2023-10-03
leanprover-community-mathlib4-bot cd52362
Merge master into nightly-testing
leanprover-community-mathlib4-bot bb61fc9
Merge master into nightly-testing
leanprover-community-mathlib4-bot da7d4a9
Merge master into nightly-testing
leanprover-community-mathlib4-bot 2c3b2d9
Merge master into nightly-testing
leanprover-community-mathlib4-bot a19f0b8
Merge master into nightly-testing
leanprover-community-mathlib4-bot 587136a
chore: bump to nightly-2023-10-04
leanprover-community-mathlib4-bot f063bb0
Merge master into nightly-testing
leanprover-community-mathlib4-bot 52b4e81
Merge master into nightly-testing
leanprover-community-mathlib4-bot 431e30e
Merge master into nightly-testing
leanprover-community-mathlib4-bot f3b3f78
Merge master into nightly-testing
leanprover-community-mathlib4-bot bc7de07
Merge master into nightly-testing
leanprover-community-mathlib4-bot 3546e57
Merge master into nightly-testing
leanprover-community-mathlib4-bot 251fbc1
chore: disable CI cache check for lean-pr-testing-NNNN branches
semorrison baf157b
Merge branch 'disable-cache-check-for-pr-testing-branches' into night…
semorrison 41a757c
Merge master into nightly-testing
leanprover-community-mathlib4-bot f55b9b8
Merge master into nightly-testing
leanprover-community-mathlib4-bot 0b59010
Merge master into nightly-testing
leanprover-community-mathlib4-bot 5d3ecd8
chore: bump to nightly-2023-10-05
leanprover-community-mathlib4-bot 969003a
Merge master into nightly-testing
leanprover-community-mathlib4-bot c94fd23
Merge master into nightly-testing
leanprover-community-mathlib4-bot 7e85b50
Merge master into nightly-testing
leanprover-community-mathlib4-bot 87a3fd4
Merge master into nightly-testing
leanprover-community-mathlib4-bot ca3520b
Merge master into nightly-testing
leanprover-community-mathlib4-bot b353b78
Merge master into nightly-testing
leanprover-community-mathlib4-bot 8725699
Merge master into nightly-testing
leanprover-community-mathlib4-bot 983e8bb
Merge master into nightly-testing
leanprover-community-mathlib4-bot 016a010
feat: first isomorphism theorem for rings
PatrickMassot 65b0898
Merge master into nightly-testing
leanprover-community-mathlib4-bot c270770
Merge master into nightly-testing
leanprover-community-mathlib4-bot 70df9a8
Merge master into nightly-testing
leanprover-community-mathlib4-bot 2368315
Merge master into nightly-testing
leanprover-community-mathlib4-bot b8ed113
Merge master into nightly-testing
leanprover-community-mathlib4-bot 5e1c56f
Merge master into nightly-testing
leanprover-community-mathlib4-bot 7ecc5c8
Merge master into nightly-testing
leanprover-community-mathlib4-bot 24b521a
Merge master into nightly-testing
leanprover-community-mathlib4-bot cb06212
Merge master into nightly-testing
leanprover-community-mathlib4-bot 9114ef9
chore: bump to nightly-2023-10-07
leanprover-community-mathlib4-bot 3c4d859
Merge master into nightly-testing
leanprover-community-mathlib4-bot cb64e48
Merge master into nightly-testing
leanprover-community-mathlib4-bot 8bace51
Merge master into nightly-testing
leanprover-community-mathlib4-bot 8b8cd5c
Merge master into nightly-testing
leanprover-community-mathlib4-bot 29a2150
chore: bump to nightly-2023-10-08
leanprover-community-mathlib4-bot f3ec698
Merge master into nightly-testing
leanprover-community-mathlib4-bot 68dfbe2
Merge master into nightly-testing
leanprover-community-mathlib4-bot 81f92b1
merge?
semorrison cde9169
Revert "feat: first isomorphism theorem for rings"
semorrison ef0c457
re-sync with master after a force push to master
semorrison ff08040
Merge master into nightly-testing
leanprover-community-mathlib4-bot b3a43a1
Merge master into nightly-testing
leanprover-community-mathlib4-bot a7908e9
Merge master into nightly-testing
leanprover-community-mathlib4-bot dafe0a8
Merge master into nightly-testing
leanprover-community-mathlib4-bot e4b43a3
Merge master into nightly-testing
leanprover-community-mathlib4-bot aaf2bdd
chore: bump to nightly-2023-10-09
leanprover-community-mathlib4-bot defdd7b
Merge master into nightly-testing
leanprover-community-mathlib4-bot 19bb0e5
Merge master into nightly-testing
leanprover-community-mathlib4-bot bcc268d
Merge master into nightly-testing
leanprover-community-mathlib4-bot 96999df
Merge master into nightly-testing
leanprover-community-mathlib4-bot 04f3972
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6ccfb14
Merge master into nightly-testing
leanprover-community-mathlib4-bot 02fb575
Merge master into nightly-testing
leanprover-community-mathlib4-bot 541b07b
Merge master into nightly-testing
leanprover-community-mathlib4-bot 2565d25
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6825846
Merge master into nightly-testing
leanprover-community-mathlib4-bot 2994c98
start fresh
semorrison ad25ba0
regressions
semorrison 24f8157
chore: bump to nightly-2023-10-10
leanprover-community-mathlib4-bot 31bbb2b
Merge master into nightly-testing
leanprover-community-mathlib4-bot fe477aa
Merge master into nightly-testing
leanprover-community-mathlib4-bot 03e0eb0
Merge master into nightly-testing
leanprover-community-mathlib4-bot 5a1da91
Merge master into nightly-testing
leanprover-community-mathlib4-bot 7f5c163
Merge master into nightly-testing
leanprover-community-mathlib4-bot 322700f
Merge master into nightly-testing
leanprover-community-mathlib4-bot c467659
Trigger CI for https://github.com/leanprover/lean4/pull/2644
leanprover-community-mathlib4-bot 34926f5
Merge master into nightly-testing
leanprover-community-mathlib4-bot 9081f93
Merge master into nightly-testing
leanprover-community-mathlib4-bot 7e3af34
Merge master into nightly-testing
leanprover-community-mathlib4-bot 031ff47
chore: bump to nightly-2023-10-11
leanprover-community-mathlib4-bot 85684b2
fixes
semorrison 4174794
Merge master into nightly-testing
leanprover-community-mathlib4-bot 4f9ad48
Merge master into nightly-testing
leanprover-community-mathlib4-bot 2b62029
Merge master into nightly-testing
leanprover-community-mathlib4-bot 1cb772e
Merge master into nightly-testing
leanprover-community-mathlib4-bot 412c3fe
Merge master into nightly-testing
leanprover-community-mathlib4-bot c7e612c
Merge master into nightly-testing
leanprover-community-mathlib4-bot 9bb8b57
Merge master into nightly-testing
leanprover-community-mathlib4-bot 6e6e777
Merge master into nightly-testing
leanprover-community-mathlib4-bot c05c82f
fix
mattrobball 9b84ecf
Merge master into nightly-testing
leanprover-community-mathlib4-bot 08ab8e2
lint
mattrobball db18a31
clean up
mattrobball 602fa7f
counterex
mattrobball 478576c
archive
mattrobball 57a8120
Merge master into nightly-testing
leanprover-community-mathlib4-bot a491559
Merge master into nightly-testing
leanprover-community-mathlib4-bot 187563b
chore: bump to nightly-2023-10-12
leanprover-community-mathlib4-bot c649ca9
use patched aesop
semorrison a5befd2
Merge master into nightly-testing
leanprover-community-mathlib4-bot 3f8fa4d
Merge master into nightly-testing
leanprover-community-mathlib4-bot a725cd9
Merge master into nightly-testing
leanprover-community-mathlib4-bot dc22ac5
Merge master into nightly-testing
leanprover-community-mathlib4-bot b758e1d
Merge master into nightly-testing
leanprover-community-mathlib4-bot 5293a8e
merge
semorrison 0bd81a1
Flag modifications dure to leanprover/lean4#2644
PatrickMassot 47e0ed2
reviewdog whitespace fixes
semorrison 062fbd7
Update Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
semorrison 1d59d17
remove another no-op simpNF
eric-wieser 1ba14a7
simps hack
eric-wieser a77c332
add a simpNF comment
eric-wieser 6f28a6c
Revert "simps hack"
mattrobball 99e242b
review comments
mattrobball 942f999
whitespace
mattrobball bd32f9a
review comments + epsilon
mattrobball d90aa6a
more clean up
mattrobball 1c87c93
clean up some more
mattrobball 5fbda93
fix long line
semorrison b3dba86
Update Mathlib/Algebra/Category/GroupCat/Biproducts.lean
semorrison 13a103f
Update Mathlib/Algebra/Category/GroupCat/Biproducts.lean
semorrison 5c02767
comments
semorrison 4a2d306
Merge branch 'lean-pr-testing-2644' of github.com:leanprover-communit…
semorrison 4afb4ea
comments
semorrison dbb1436
fix comments
semorrison 73f0566
fixes
semorrison 35cdd1c
fixes
semorrison ffa5702
more
semorrison 740abe2
Update Mathlib/Order/InitialSeg.lean
semorrison 11ef6da
suggestions from review
semorrison File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If
ε
is an implementation detail, then presumably we can uselocal simp
here?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Feel free to make such changes yourself, but otherwise I'm going to leave these for "later".