[Merged by Bors] - feat: port ZFC set intersection #3345
Closed
Conversation
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
vihdzp
added
awaiting-review
mathlib3-pair
kim-em
added
blocked-by-other-PR
bors bot
pushed a commit
to leanprover-community/mathlib3
that referenced
this pull request
Apr 25, 2023
It now matches `coe_sUnion`, and works as a `norm_cast` lemma. Mathlib 4: leanprover-community/mathlib4#3345
kim-em
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
Parcly-Taxel
removed
the
merge-conflict
YaelDillies
approved these changes
May 1, 2023
There was a problem hiding this comment.
This forward-port is a bit of a mess because bits of leanprover-community/mathlib3#18232 were already ported, and this forward-port fixes a few names and wrapping, but I've now checked both resulting files by hand and can safely say they match.
maintainer merge
|
bors r+ |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
May 1, 2023
Also fixes some erroneous theorem names from the port. [`set_theory.zfc.basic`@`98bbc3526516bca903bff09ea10c4206bf079e6b`..`f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a`](https://leanprover-community.github.io/mathlib-port-status/file/set_theory/zfc/basic?range=98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a) Mathlib 3: leanprover-community/mathlib3#18232 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
alexjbest
added a commit
that referenced
this pull request
May 3, 2023
fail if unchanged fix new version feat: port LinearAlgebra.Matrix.Diagonal (#3695) Some proofs in the last section were failing even with eta-experiment, so I generalized some lemmas from `Field`s to `Semifield`s. chore: update SHA (#3711) I forgot to update the SHA in #3675 chore: Rename to `AddLocalization` (#3714) This name wasn't properly capitalised. chore: forward-port leanprover-community/mathlib3#18880 (#3717) feat: make alias compile code when possible (#3719) feat: port LinearAlgebra.SymplecticGroup (#3696) chore: add hash for Data.MvPolynomial.Polynomial (#3723) feat: port LinearAlgebra.ProjectiveSpace.Basic (#3692) feat: allow several tactics on types that are slightly less obviously Types (#3682) Many tactics attempt to get the universe of the sort of the terms involved by matching on the level being a succ of something. Unfortunately this fails on some nontrivial examples like mvpolynomial which can have type `Sort (max (u+1) (v+1))` Instead we decrement the level manually after matching it. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60ring.60.20tactic.20cannot.20prove.20equality.20about.20.60MvPolynomial.60/near/352549549 This PR modifies ring, ring_nf, nontriviality, polyrith, linarith, and some norm_num handlers to appropriately handle this. Test cases showing examples that failed before (inspired by the case of mvpolynomial, but in principle there could be other interesting types that have multiple universe parameters in this way, some of which may even have a linear order who knows). In doing so we factor out `inferTypeQ'` into its own file `Mathlib.Tactic.Qq` for mathlib-relevant extensions of Qq feat: port CategoryTheory.Abelian.Transfer (#3424) chore: Remove `finset.sup_finset_image` (#3713) Match leanprover-community/mathlib3#18893 Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> fix: allow library_search to run when maxHeartbeats = 0 (#3720) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> fix: find MathlibExtras from downstream projects (#3721) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> feat: port LinearAlgebra.ProjectiveSpace.Independence (#3728) Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> feat: `a * b ≠ b ↔ a ≠ 1` (#3726) leanprover-community/mathlib3#18635 * [`algebra.group.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..84771a9f5f0bd5e5d6218811556508ddf476dcbd) * [`algebra.order.field.basic`@`44e29dbcff83ba7114a464d592b8c3743987c1e5`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/field/basic?range=44e29dbcff83ba7114a464d592b8c3743987c1e5..84771a9f5f0bd5e5d6218811556508ddf476dcbd) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> chore: no newline before aligns (#3735) Co-authored-by: Moritz Firsching <firsching@google.com> feat: port CategoryTheory.Monad.Coequalizer (#3733) feat: port AlgebraicTopology.ExtraDegeneracy (#3729) feat: port Algebra.Category.Group.ZModuleEquivalence (#3732) feat: port FieldTheory.Tower (#3716) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> chore: move theorems on `String` to std4 (#3712) leanprover-community/batteries#124 moves the following from Mathlib4 to Std4: * helper `simp` theorems on `String.Pos` * `String.utf8GetAux.inductionOn` feat: annotate build errors in the github files changed tab using an action (#3739) This is suboptimal as it doesn't handle multiline comments, but it is better than nothing, and the implementation works out of the box. This is broadly similar to the support we had in mathlib 3, but the implementation is different as we no longer have json errors as an option, so must instead match an errorformat directly (the gcc one works fine). Supporting multiline error messages appears not to be possible using the builtin output without further processing with the current state of problem matchers supported by github (which follow the vscode design). Thus to get an improvement on this the build output must be piped through a second program that processes it in some way, or a lake build type command should be added that outputs in a required format. Likewise to get annotations for linter failures we will need to add extra information to the linter output, either setting the annotations ourselves (as we did in mathlib 3) or at least adding line numbers to the existing output so that we can at least match it with a problem matcher again. feat: port Topology.Category.Profinite.Basic (#3705) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: adamtopaz <github@adamtopaz.com> feat: port ZFC set intersection (#3345) Also fixes some erroneous theorem names from the port. [`set_theory.zfc.basic`@`98bbc3526516bca903bff09ea10c4206bf079e6b`..`f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a`](https://leanprover-community.github.io/mathlib-port-status/file/set_theory/zfc/basic?range=98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a) Mathlib 3: leanprover-community/mathlib3#18232 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> feat: port Mathlib.Data.Ordmap.Ordnode (#1455) Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr> feat: port Topology.Category.Profinite.Projective (#3746) feat: `f.update i '' Icc a b = Icc (f.update i a) (f.update i b)` (#3747) Match leanprover-community/mathlib3#18892 * [`order.lattice`@`d6aad9528ddcac270ed35c6f7b5f1d8af25341d6`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/order/lattice?range=d6aad9528ddcac270ed35c6f7b5f1d8af25341d6..e4bc74cbaf429d706cb9140902f7ca6c431e75a4) * [`algebra.group.pi`@`90df25ded755a2cf9651ea850d1abe429b1e4eb1`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=90df25ded755a2cf9651ea850d1abe429b1e4eb1..e4bc74cbaf429d706cb9140902f7ca6c431e75a4) * [`data.set.intervals.pi`@`4020ddee5b4580a409bfda7d2f42726ce86ae674`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/intervals/pi?range=4020ddee5b4580a409bfda7d2f42726ce86ae674..e4bc74cbaf429d706cb9140902f7ca6c431e75a4) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> enhance: `fail_if_no_progress` * evaluates tactics given instead of running them on the main goal * uses config to specify/restrict progress check test: basic config tests minor fixes does it work? styl fixes fixes and name more fixes Revert "Merge remote-tracking branch 'origin/fail_if_no_progress' into alexjbest/simprw-fail" This reverts commit 224bd3e, reversing changes made to a3742b4. remove usage of fail if no progress
kim-em
pushed a commit
that referenced
this pull request
May 10, 2023
Also fixes some erroneous theorem names from the port. [`set_theory.zfc.basic`@`98bbc3526516bca903bff09ea10c4206bf079e6b`..`f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a`](https://leanprover-community.github.io/mathlib-port-status/file/set_theory/zfc/basic?range=98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a) Mathlib 3: leanprover-community/mathlib3#18232 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
hrmacbeth
pushed a commit
that referenced
this pull request
May 10, 2023
Also fixes some erroneous theorem names from the port. [`set_theory.zfc.basic`@`98bbc3526516bca903bff09ea10c4206bf079e6b`..`f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a`](https://leanprover-community.github.io/mathlib-port-status/file/set_theory/zfc/basic?range=98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a) Mathlib 3: leanprover-community/mathlib3#18232 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
hrmacbeth
pushed a commit
that referenced
this pull request
May 11, 2023
Also fixes some erroneous theorem names from the port. [`set_theory.zfc.basic`@`98bbc3526516bca903bff09ea10c4206bf079e6b`..`f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a`](https://leanprover-community.github.io/mathlib-port-status/file/set_theory/zfc/basic?range=98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a) Mathlib 3: leanprover-community/mathlib3#18232 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
mattrobball
added a commit
that referenced
this pull request
May 18, 2023
commit 8377ae6b176cc857b383b04173fa5577d09f1689
Author: Matthew Ballard <matt@mrb.email>
Date: Wed May 17 21:16:04 2023 -0400
update mathlib.lean
commit 8d909eb33ad5e164db2deaf8444b0a21351ec99f
Author: Matthew Ballard <matt@mrb.email>
Date: Wed May 17 21:14:55 2023 -0400
lint
commit 6bcb7f5e70763e15c405912988d867fbe0637691
Author: Matthew Ballard <matt@mrb.email>
Date: Wed May 17 21:10:16 2023 -0400
fix last errors
commit 1b85bed8887c82368d7da6f4189aea86e98991cb
Author: Scott Morrison <scott.morrison@gmail.com>
Date: Thu May 18 10:46:42 2023 +1000
fixes
commit 519af1d828205304827466024ee65506eb99186e
Merge: 98bf9f9b 8bf78812
Author: Scott Morrison <scott.morrison@gmail.com>
Date: Thu May 18 09:09:10 2023 +1000
Merge remote-tracking branch 'origin/master' into port/CategoryTheory.Bicategory.Free
commit 98bf9f9b293dfe099a631c3bda0bd5e493a7d49e
Merge: 1910c612 f9ae3115
Author: Matthew Ballard <matt@mrb.email>
Date: Sat May 13 08:31:30 2023 -0400
Merge branch 'master' into port/CategoryTheory.Bicategory.Free
commit 1910c612e2e43e3c263f68996ed72b9ac5204f6e
Author: Matthew Ballard <matt@mrb.email>
Date: Sat May 13 08:31:19 2023 -0400
add new file
commit 7af7463b52e7a6d69eb7478235117c023ec8c6aa
Merge: f0adc533 269fb63e
Author: Matthew Ballard <matt@mrb.email>
Date: Sat May 13 08:29:53 2023 -0400
Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory.Bicategory.Free' into port/CategoryTheory.Bicategory.Free
commit 269fb63e9215d34da56d0b4a7288aca3bde89bc0
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Wed May 10 05:02:09 2023 +0000
feat: port Analysis.Normed.Group.ControlledClosure (#3880)
commit 628125292856eb71f72eeecd4f5f967f006ec773
Author: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Wed May 10 05:02:09 2023 +0000
feat: add some `pp_extended_field_notation`s (#3592)
Add some `pp_extended_field_notation`, for opt-in cases with additional arguments.
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
commit 21708212ef62b7ac824871864a8c3d103f320750
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Wed May 10 04:45:22 2023 +0000
feat: port Topology.ContinuousFunction.LocallyConstant (#3877)
commit 5d84f9b67af72c588b96bb7821b2523f821b1bec
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Wed May 10 01:01:27 2023 +0000
feat: port MeasureTheory.Covering.VitaliFamily (#3867)
commit 4f3e6145116f5ddf98f9f2615f7e4b129bd02dce
Author: Matthew Robert Ballard <matt@mrb.email>
Date: Wed May 10 01:01:26 2023 +0000
feat: port Algebra.Category.Group.EquivalenceGroupAddGroup (#3861)
commit 0d738a8fef346fb7f9020b327b61fe7f422d1524
Author: Pol_tta <pol_tta@outlook.jp>
Date: Wed May 10 01:01:24 2023 +0000
feat: port Dynamics.Ergodic.MeasurePreserving (#3821)
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: MonadMaverick <MonadMaverick@pm.me>
commit 9c00193316232966719be6916399504da82103c7
Author: Pol_tta <MonadMaverick@pm.me>
Date: Wed May 10 01:01:22 2023 +0000
feat: port MeasureTheory.Measure.OpenPos (#3820)
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
commit 55413d4565e6e33a8ff7065b20a3f3f9ba18fc0d
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Wed May 10 00:18:41 2023 +0000
feat: port Analysis.Convex.PartitionOfUnity (#3868)
commit 468ee3fa8c1a4a81a0a1ce5829afc0e65226ea97
Author: Pol_tta <pol_tta@outlook.jp>
Date: Wed May 10 00:18:39 2023 +0000
feat: port MeasureTheory.Lattice (#3824)
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: MonadMaverick <MonadMaverick@pm.me>
commit 01d44eab0e102b78434bd20142f8e1db75e22599
Author: Pol_tta <MonadMaverick@pm.me>
Date: Wed May 10 00:18:37 2023 +0000
feat: port MeasureTheory.Measure.MutuallySingular (#3818)
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
commit 3b3411e0739d9a22e8cabc54b724123a8d773333
Author: Kyle Miller <kmill31415@gmail.com>
Date: Wed May 10 00:18:35 2023 +0000
feat: pp_extended_field_notation command to pretty print with dot notation (#3811)
The projection notation delaborator that comes from core Lean has some limitations. We introduce a new projection notation delaborator that is able to collapse parent projection sequences, for example `x.toC.toB.toA.val` into `x.val`.
The other limitation of the delaborator is that it can only handle true projections that do not have any additional arguments. This commit adds a `pp_extended_field_notation` command to switch on projection notation for specific functions. This command defines app unexpanders that pretty print that function application using dot notation.
The app unexpander it produces has a small hack to completely collapse parent projection sequences. Since it is an app unexpander, we do not have access to the actual types, so we use a heuristic that, for example with `A.foo`, if we are looking at `A.foo x.toA y z ...` then we can pretty print this as `x.foo y z`. The projection delaborator is able to collapse parent projection sequences except for the vary last one, so this finishes it off. Note that this heuristic can lead to output that does not round trip if there is a `toA` function that is not a parent projection that happens to be pretty printed with dot notation.
commit 7341d34cb0b1173f04f03c7f51daea36a230e35c
Author: David Loeffler <d.loeffler.01@cantab.net>
Date: Tue May 9 23:59:30 2023 +0000
feat: port Analysis.NormedSpace.CompactOperator (#3805)
commit c10b02b9f02a8d212f1ab2cdd18440785e464c58
Author: Scott Morrison <scott@tqft.net>
Date: Tue May 9 23:06:55 2023 +0000
feat: port CategoryTheory.Functor.Flat (#3703)
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
commit 64b7fb14e6a9085f2a3e6fa5bcce317a7120cc3a
Author: Pol_tta <MonadMaverick@pm.me>
Date: Tue May 9 19:44:35 2023 +0000
feat: port MeasureTheory.Measure.AEMeasurable (#3819)
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
commit 15da6c20b0e9b06b46b5c6b325f7d21be2d568b7
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Tue May 9 10:06:14 2023 +0000
feat: port Probability.ProbabilityMassFunction.Basic (#3865)
commit 8ecbd9569ffd605712cd21b65d0d8864520dfb66
Author: Matthew Robert Ballard <matt@mrb.email>
Date: Tue May 9 10:06:13 2023 +0000
feat: port CategoryTheory.Preadditive.InjectiveResolution (#3860)
Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
commit da3993ff939d796018ff5e95c41712d1975abfa8
Author: Matthew Robert Ballard <matt@mrb.email>
Date: Tue May 9 10:06:12 2023 +0000
feat: port Topology.Category.Top.Limits.Konig (#3853)
Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
commit c3bace0cd04c23c1dd9ab361b03eb80faa8e2c3d
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Tue May 9 09:46:42 2023 +0000
feat: port MeasureTheory.Measure.Sub (#3866)
commit 99bb9fb7ca74cba20b2c2588d2fb9595e5cb98b7
Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Tue May 9 08:58:57 2023 +0000
feat port: LinearAlgebra.ProjectiveSpace.Subspace (#3832)
commit f273bff58209ed6273afcaf85b7bc554a7ceac3a
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Tue May 9 06:29:09 2023 +0000
chore: tidy various files (#3848)
commit cfbec6e28f4c3d117debf58d1338e531cb90a3aa
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Tue May 9 06:12:54 2023 +0000
feat: port Topology.PartitionOfUnity (#3863)
commit 37807d6a99a0199676e029358f20ac5738d9639f
Author: Matthew Robert Ballard <matt@mrb.email>
Date: Tue May 9 06:12:53 2023 +0000
feat: port CategoryTheory.Preadditive.Injective (#3859)
commit b75c4d73f2b15b8234a5dcdca62ad160ae9caf76
Author: Matthew Robert Ballard <matt@mrb.email>
Date: Tue May 9 06:12:52 2023 +0000
feat: port Topology.Category.Top.Limits.Cofiltered (#3855)
commit b1ee18a7fb8e0079cb0c0fd0fea1afd019219fe5
Author: David Renshaw <dwrenshaw@gmail.com>
Date: Tue May 9 06:12:51 2023 +0000
fix: remove unneeded LibrarySearch import (#3854)
Removes from `Analysis/SpecificLimits/Normed.lean` an `import Mathlib.Tactic.LibrarySearch` that was accidentally included in #3419.
commit 4ddbf238481366ca34965e9d10278833f01a3e70
Author: MonadMaverick <MonadMaverick@pm.me>
Date: Tue May 9 05:50:38 2023 +0000
feat: port MeasureTheory.Measure.MeasureSpace (#3324)
This PR also renames instances in `MeasureTheory.MeasurableSpace`.
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
commit d52008fd7cc8539b1d1b32c9eac2b0aeac276244
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Mon May 8 22:44:20 2023 +0000
fix: make `ConcreteCategory.Forget` reducible (#3857)
This seems to help in downstream files, [See Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/typeclass.20inference.20not.20seeing.20through.20reducible.20definition/near/356130343)
commit a627d110cd7b94a4308c2c71a46f9ed44930bb97
Author: Christopher Hoskin <christopher.hoskin@gmail.com>
Date: Mon May 8 21:09:37 2023 +0000
feat: port Topology.ContinuousFunction.Algebra (#3332)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
commit 6863ef07ca5aa72edacb87d14977f8816aa3951d
Author: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Mon May 8 19:26:28 2023 +0000
chore(*): tweak priorities for linear algebra (#3840)
We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`,
as this is a path which is followed all the time in linear algebra where the defining semilinear map
`σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module
definition depends on the `Semiring` structure.
Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last
declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so
that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`.
commit a25c78e5c93a3217b9ee46882955746f08469791
Author: Scott Morrison <scott@tqft.net>
Date: Mon May 8 13:36:25 2023 +0000
chore: fix name in Mathlib.Topology.Algebra.Module (#3850)
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
commit 51e2e32cd407e1965885af13d1a9bb96e0709c05
Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Mon May 8 11:53:12 2023 +0000
feat port: Topology.Algebra.Nonarchimedean.AdicTopology (#3826)
commit a5f2b200a2c1fb019a358e347353e19f09402bd5
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Mon May 8 11:21:34 2023 +0000
feat: port Data.Complex.Orientation (#3849)
commit 2906eb7cfd4f8b36322c63e0209c06e0353a5261
Author: Pol_tta <pol_tta@outlook.jp>
Date: Mon May 8 10:01:09 2023 +0000
feat: port MeasureTheory.Tactic (#3816)
commit b5c7cda33ead3895a3e92b9b41112bdc755a433a
Author: Jujian Zhang <jujian.zhang1998@outlook.com>
Date: Mon May 8 09:17:50 2023 +0000
feat: definition of krull dimension for a preordered set (#3704)
Given a preordered set $(S, <)$, the krull dimension of $S$ is defined to be $\sup\{n | a_0 < a_1 < ... < a_n\}$ where the supremum takes place in extended natural numbers $\mathbb N \cup \{\pm \infty\}$, i.e. empty set is negative-infinite dimensional and a set with arbitrary long $a_0 < a_1 < ... < a_n$ is positive dimensional.
Similar constructions in mathlib does require a chain to be nonempty so that empty set would have the wrong dimension, so I defined a new structure `StrictSeries` to avoid confusion with `chain`; in this structure, the underlying list is always nonempty.
commit 8685958b7012efbeb848057bc4b936aaa4c39b63
Author: Pol_tta <pol_tta@outlook.jp>
Date: Mon May 8 05:55:43 2023 +0000
fix: remove lambda abstraction of `Nat.rec_zero` and `Nat.rec_add_one` (#3839)
```lean
theorem rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) :
(Nat.rec h0 h : ∀ n, C n) 0 = h0 :=
rfl
```
The above theorem is elaborated as follow:
```lean
theorem rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) :
(fun n => Nat.rec h0 h n) 0 = h0 :=
rfl
```
This form of the theorem isn't generic. This PR fixes this problem.
Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com>
commit b840606e7074798762c81e73e53ac4ab2e661de5
Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Mon May 8 05:55:41 2023 +0000
feat port: LinearAlgebra.Orientation (#3777)
I had to add a bunch of `set_option synthInstance.etaExperiment true`, `set_option maxHeartbeats` and `set_option synthInstance.maxHeartbeats` to this file
I tried to use the methods described in this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/maxHeartbeats/near/356217898) to remove some of the `maxHeartbeats` but I was not successful.
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
commit 882005842a71af115186357b21dd4f2bbfe2a597
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Mon May 8 05:55:40 2023 +0000
feat: port Analysis.SpecificLimits.Normed (#3419)
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
commit c2cf5ba958fb0ac9b1536f66d98b73a486aabaee
Author: Pol_tta <pol_tta@outlook.jp>
Date: Mon May 8 03:29:54 2023 +0000
fix: `lift` can't be used when the type of the goal is `Sort.{?u}` while `?u` is assigned by `0` (#3800)
For example, this emits error.
```lean
example (n : ℕ) : n = 0 ∨ ∃ p : ℕ+, n = p := by
by_cases hn : 0 < n
· lift n to ℕ+ using hn -- error
right
exact ⟨n, rfl⟩
· left
exact Nat.eq_zero_of_nonpos _ hn
```
The cause is that `lift` doesn't instantiate level metavariables when checking that the type of the goal is `Prop`.
This PR makes the above example available. Please refer to `test/lift.lean`.
commit 3dd4e55886338c90af2571a024a0418d4fe6b09a
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Mon May 8 03:29:53 2023 +0000
feat: port Data.Sym.Card (#3109)
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
commit 016b02ed781f7804fe6c002d33eabc205a5e30de
Author: Pol_tta <pol_tta@outlook.jp>
Date: Mon May 8 03:07:17 2023 +0000
feat: port Computability.Partrec (#3830)
commit 28e49fca3bcedc90c9149a26c10c338ebc00d7a5
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Mon May 8 02:51:12 2023 +0000
feat: port Topology.Category.Top.OpenNhds (#3834)
commit a5a10ca18c91a12454b6317e637d69586c33448c
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Mon May 8 00:54:18 2023 +0000
chore: forward-port leanprover-community/mathlib#18878 (#3742)
commit 4350c4e364eda158598503baf5916729406f4e95
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Mon May 8 00:54:17 2023 +0000
feat: port Analysis.Normed.Group.Quotient (#3457)
Co-authored-by: Mauricio Collares <mauricio@collares.org>
commit cd0670b6fbe9fc3398ce064cd55f7464e15d7353
Author: Moritz Doll <moritz.doll@googlemail.com>
Date: Mon May 8 00:35:14 2023 +0000
chore: add explicit name for instances in Analysis.Seminorm (#3759)
Some names were extremely long.
Example: [Seminorm.instConditionallyCompleteLatticeSeminormToSeminormedRingToSeminormedCommRingToNormedCommRingToAddGroupToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToFieldToSMulWithZeroToMonoidWithZeroToSemiringToDivisionSemiringToMulActionWithZeroToAddCommMonoid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Seminorm.html#Seminorm.instConditionallyCompleteLatticeSeminormToSeminormedRingToSeminormedCommRingToNormedCommRingToAddGroupToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToFieldToSMulWithZeroToMonoidWithZeroToSemiringToDivisionSemiringToMulActionWithZeroToAddCommMonoid)
commit 6045f2042e5e14e3b45a9ca56bf2be04921827dd
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Sun May 7 14:02:40 2023 +0000
feat: port Algebra.ContinuedFractions.Computation.Translations (#3794)
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
commit 0285c2bf3919356b608125ae878487201d15b488
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Sun May 7 13:25:52 2023 +0000
chore: forward port leanprover-community/mathlib#18951 (#3837)
commit 0633b89bb4e7148fcb22a6c26915d79838a11ad5
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Sun May 7 09:18:13 2023 +0000
chore: forward port leanprover-community/mathlib#18866 (#3813)
commit b3b1b7dd2388506eceadab75d83ca8183aeeb496
Author: Scott Morrison <scott@tqft.net>
Date: Sun May 7 09:18:12 2023 +0000
feat: library_search tries most specific lemmas first, and then those with shorter names first (#3725)
It turns out that `DiscrTree.getMatch` returns more specific results later than less specific ones, and so we want to put a `.reverse` in, as `library_search` is more likely to be able to make use of the more specific lemmas.
Additionally, within each "batch" of lemmas in the DiscrTree, we sort them so that those with shorter names are tried before those with longer names. You shouldn't expect this to be anymore successful, I think, but maybe the user will be happier getting shorter results rather than longer ones.
See some further discussion at [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20timeout/near/356406350).
- [x] depends on: #3771
[](https://gitpod.io/from-referrer/)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
commit c993a4e8f1a1d2c587b3d939af778d3bf3dff420
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Sun May 7 08:52:06 2023 +0000
chore: forward port leanprover-community/mathlib#18479 (#3829)
commit 038caab459760a87b476351dfd62b7ab2a50bee5
Author: Scott Morrison <scott@tqft.net>
Date: Sun May 7 08:35:59 2023 +0000
feat: speedup library_search by using two DiscrTrees (#3771)
Previously, `library_search` used a single `DiscrTree`. There is a cached `DiscrTree` covering the whole library (and which is cached to disk), and then when we call `library_search`, we traverse the declarations in the current file, adding those into that `DiscrTree`.
This PR speeds up that process by using a second independent `DiscrTree` for the declarations in the current file. This means that the cached tree for the library does not need to be "edited in place", and so we save some time.
On the test file on my computer this speeds up from around 10.0s to around 8.2s. When calling `library_search` low down in a large file we should expect larger gains.
The PR also does some refactoring work on `DeclCache`, which will be useful if/when we install global caching for other lookup tactics such as `propose` or [`rewrites`](https://github.com/leanprover-community/mathlib4/pull/3119).
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
commit 18c6e24d4a7c5ec87e4c7e9e295e852475c70c55
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Sun May 7 07:13:52 2023 +0000
chore: forward-port leanprover-community/mathlib#18934 (#3806)
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
commit 424263023c2e9c1588f05d9a28a5abb9ae8ae88b
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Sun May 7 07:13:51 2023 +0000
chore: forward-port leanprover-community/mathlib#18902 (#3770)
commit 8a2c2bf047940fdad965814424f3a2c1d8a6644d
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Sun May 7 05:02:30 2023 +0000
chore: bye-bye, solo `by`s! (#3825)
This PR puts, with one exception, every single remaining `by` that lies all by itself on its own line to the previous line, thus matching the current behaviour of `start-port.sh`. The exception is when the `by` begins the second or later argument to a tuple or anonymous constructor; see https://github.com/leanprover-community/mathlib4/pull/3825#discussion_r1186702599.
Essentially this is `s/\n *by$/ by/g`, but with manual editing to satisfy the linter's max-100-char-line requirement. The Python style linter is also modified to catch these "isolated `by`s".
commit 2d3d9fe6f82530f0355cf06d52cfa44bfbb1a033
Author: Hagb (Junyu Guo 郭俊余) <hagb@hagb.name>
Date: Sat May 6 19:50:27 2023 +0000
feat(Data/MvPolynomial/Basic): add and generalize some lemmas from Finsupp and MonoidAlgebra (#3604)
Most of these changes generalize from `DistribMulAction` to `SmulZeroClass`.
The new lemmas are all just proved using corresponding lemmas on the underlying types.
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
commit 55705f9084276a7a7de523230af1827ba60fb949
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Sat May 6 19:21:52 2023 +0000
ci: make bors block on the check_imported job (#3827)
commit f72485cdca5b6010514168873616232d7765dc90
Author: Scott Morrison <scott@tqft.net>
Date: Sat May 6 15:10:58 2023 +0000
chore: bump to Lean 4 nightly-2023-05-06 (#3817)
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
commit f1ae5b7ec8d705042684482b8fb06cd34adfcb65
Author: Scott Morrison <scott@tqft.net>
Date: Sat May 6 12:10:21 2023 +0000
feat: enable cancel_denoms preprocessor in linarith (#3801)
Enable the `cancelDenoms` preprocessor in `linarith`. Closes #2714.
- [x] depends on: #3797
[](https://gitpod.io/from-referrer/)
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit ec38b915d3a36cb7d0adef661259453be01c4728
Author: MonadMaverick <pol_tta@outlook.jp>
Date: Sat May 6 11:29:51 2023 +0000
feat: port MeasureTheory.Measure.NullMeasurable (#3349)
Co-authored-by: MonadMaverick <MonadMaverick@pm.me>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
commit d8f1f02fd6a548ea4d1f944972a929089cca5869
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Sat May 6 08:46:32 2023 +0000
chore: forward port leanprover-community/mathlib#18910 (#3814)
commit 79ca50dced9a0a479fd0da6941f7cd67a9927d9e
Author: Patrick Massot <patrickmassot@free.fr>
Date: Sat May 6 08:46:30 2023 +0000
feat: `cancel_denoms` tactic (#3797)
Ports the tactic `CancelDenoms.derive` and the interactive tactic `cancel_denoms`. This tactic is needed to make `linarith` handle divisions by numbers, but this PR does not involve `linarith`.
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
commit b7ed6f5bb61ecc043f01aa3b27276188ba1a2cdf
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Sat May 6 08:29:50 2023 +0000
chore: fix names (#3812)
Forward-port leanprover-community/mathlib#18921 and leanprover-community/mathlib#18924
commit 0fbb715e696b40a5dfa8974c9f59a890a65fd2b7
Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Sat May 6 07:33:35 2023 +0000
feat port : RingTheory.Ideal.AssociatedPrime (#3810)
commit a31acfcf3520728bef79bcfa4e0275466a0834ab
Author: EmilieUthaiwat <emiliepathum@gmail.com>
Date: Sat May 6 07:17:10 2023 +0000
feat: port LinearAlgebra.Lagrange (#3784)
commit 2617ac0e6b300c20d8bb10198fafe9332d45df5a
Author: MonadMaverick <MonadMaverick@pm.me>
Date: Sat May 6 06:40:03 2023 +0000
feat: port MeasureTheory.Measure.AEDisjoint (#3351)
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
commit 214014d2c39d5fe770fbb305588808bcb1a4aff4
Author: Scott Morrison <scott@tqft.net>
Date: Fri May 5 22:16:38 2023 +0000
chore: forward-port backports (#3752)
* `data.mv_polynomial.basic`, `data.mv_polynomial.funext`: leanprover-community/mathlib#18839
* `category_theory.limits.preserves.finite`, `category_theory.preadditive.projective`: leanprover-community/mathlib#18890
* `category_theory.abelian.basic`, `category_theory.abelian.opposite`: leanprover-community/mathlib#18740
* `topology.category.Top.limits.basic`: leanprover-community/mathlib#18871. Note that this does not show a useful diff on the dashboard pages as file splits aren't tracked well by git.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit 35f51927282d120df99e96c037ddfb4132e947bf
Author: Eric Wieser <yael.dillies@gmail.com>
Date: Fri May 5 14:00:33 2023 +0000
chore: forward-port leanprover-community/mathlib#18906 (#3798)
commit ddf1a04c942b901a07d053d2f967f2ad40777e1a
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Fri May 5 13:44:48 2023 +0000
feat: port MeasureTheory.Function.AEMeasurableSequence (#3803)
commit e0fd3f7dbf994599af312d5f630bf7fcedbb9bce
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Fri May 5 12:24:18 2023 +0000
chore: tidy various files (#3718)
commit f4dd3adaf6847e2e940853c1d3d2b36aaa781425
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri May 5 06:25:34 2023 +0000
chore: update SHA from #3753 (#3799)
I forgot to update it in #3753.
commit 963ac8132f80aa069680b719e64cb4b0cba54366
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Thu May 4 19:07:27 2023 +0000
feat: port Algebra.ContinuedFractions.ConvergentsEquiv (#3795)
commit 3a802fc9446bc158d1486997f5f5794e4c402beb
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Thu May 4 16:30:32 2023 +0000
feat: well-founded or transitive relations don't have cycles (#3793)
Match https://github.com/leanprover-community/mathlib/pull/18512
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit d9ea05decd47313168b7f7febd64643ff7ed1932
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Thu May 4 11:23:11 2023 +0000
chore: forward-port leanprover-community/mathlib#18922 (#3779)
commit 4b452a9fec289cc8ed1e18098680ab0db19079d4
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Thu May 4 11:23:10 2023 +0000
chore: forward-port leanprover-community/mathlib#18876 (#3753)
commit 45acfec0369c6720452249bdf860cbeafa89c25b
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Thu May 4 11:23:09 2023 +0000
chore: forward-port leanprover-community/mathlib#18879 (#3741)
commit 700eb94e185cb781b1f8945cb350ff3051f4a52a
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Thu May 4 09:12:04 2023 +0000
feat: port Algebra.ContinuedFractions.TerminatedStable (#3792)
Co-authored-by: Moritz Firsching <firsching@google.com>
commit d7a6de21586b9f2fd41676da624f6fc4ccd3eb18
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Thu May 4 09:12:03 2023 +0000
feat: port Algebra.ContinuedFractions.Computation.Basic (#3788)
Co-authored-by: Moritz Firsching <firsching@google.com>
commit c643d1282c5c47f210c9497d1e19867dbd1bcb74
Author: MonadMaverick <MonadMaverick@pm.me>
Date: Thu May 4 08:44:21 2023 +0000
feat: port MeasureTheory.Measure.MeasureSpaceDef (#3325)
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
commit 6ee07bd7ff39032233031f056c2649ccda4cafef
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Thu May 4 08:21:57 2023 +0000
feat: port Algebra.ContinuedFractions.ContinuantsRecurrence (#3791)
Co-authored-by: Moritz Firsching <firsching@google.com>
commit ac2e5438c8c07b7c63166df1bdf15076028c4159
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Thu May 4 05:47:35 2023 +0000
feat: port Algebra.ContinuedFractions.Translations (#3783)
Co-authored-by: Moritz Firsching <firsching@google.com>
commit e34f9b0fc494772fc304aeffa32e829278a17962
Author: Kyle Miller <kmill31415@gmail.com>
Date: Wed May 3 23:01:50 2023 +0000
feat: delaborators for Finset.prod and Finset.sum (#3772)
Also fixes some spacing in their `syntax` commands, which impacts pretty printing.
commit d490330ae628c357fe9c758990605ded66628194
Author: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Wed May 3 22:31:52 2023 +0000
chore: update Mathlib/Tactic.lean (#3727)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit 2f62a68be3bd7b099d591820492b5eb668f3843e
Author: Alex J Best <alex.j.best@gmail.com>
Date: Wed May 3 17:20:53 2023 +0000
feat: implement intermediate state for simp_rw (#3738)
closes #3680, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Stepping.20through.20simp_rw/near/326712986
commit ee67ae82322f25cafc7534b5dbd33ad93d8faa8b
Author: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Wed May 3 14:00:58 2023 +0000
refactor, fix: `MetaM` version of `rfl` tactic and missing `whnfR`/`instantiateMVars` (#3758)
This PR factors out a `MetaM` version of the `rfl` tactic and adds a missing `whnfR` and `instantiateMVars` in front of the goal type. This means that a few `rw`s across mathlib4 now close the goal instead of e.g. requiring a trailing `exact le_rfl`.
Note: we do not use `whnfR` on the return type when adding the `refl` extension in the first place, as `forallMetaTelescopeReducing` already performs `whnf` (here, at reducible transparency).
See [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233758.20.E2.80.93.20rfl.20refactor.20.26.20fix) for some discussion on the internal changes made.
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
commit 8cad0a826486d2a0005de7e353e12f2ae143b78e
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Wed May 3 13:39:19 2023 +0000
feat: port LinearAlgebra.AffineSpace.FiniteDimensional (#3670)
commit 052deed907b6ffc756bd7ce4ecdedf4d6db1068d
Author: JeEyben <124388640+JeEyben@users.noreply.github.com>
Date: Wed May 3 13:39:17 2023 +0000
feat: port RingTheory.Localization.InvSubmonoid (#3384)
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
commit 5a77592a11f98444a19c2ea97fad0291fe408b96
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Wed May 3 13:39:15 2023 +0000
feat: port Algebra.ContinuedFractions.Basic (#3379)
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
commit 8f6e4d2054a99fd8c847cacfe57b408b8b18646a
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Wed May 3 13:39:13 2023 +0000
feat: port CategoryTheory.Monoidal.Free.Basic (#2808)
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Johan Commelin <johan@commelin.net>
commit 30a890eb4e9dbda9dd9dc42c4e2f260b59abb214
Author: Scott Morrison <scott@tqft.net>
Date: Wed May 3 13:16:44 2023 +0000
fix: a missing TypeMax (#3781)
One was missed; curiously it wasn't harmful in `master`, but when we turn on `etaExperiment` globally this causes a breakage
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit 814f492f80e97836913d1b788911a1ddc76b6f42
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed May 3 12:09:25 2023 +0000
chore: move shortcut instance to Algebra.Algebra.Basic (#3778)
See https://github.com/leanprover-community/mathlib/pull/18907
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit 0ab5e61ca44a52206df99830a0facaf91d8b803e
Author: Moritz Doll <moritz.doll@googlemail.com>
Date: Wed May 3 11:33:41 2023 +0000
docs: fix names in Analysis.LocallyConvex.Bounded (#3774)
commit ac0fd896f1bb1f197f25f5f654a859b4a02d8516
Author: MonadMaverick <MonadMaverick@pm.me>
Date: Wed May 3 11:02:26 2023 +0000
feat: port MeasureTheory.Measure.OuterMeasure (#3674)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Johan Commelin <johan@commelin.net>
commit ae90d57d66ab4137eb22d9152cdd2d6aa0f19cd6
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Wed May 3 06:27:24 2023 +0000
feat: port LinearAlgebra.AffineSpace.Matrix (#3775)
commit 3ad45ada879ff7d1eb0c425df6bf8d4bec66adba
Author: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Date: Wed May 3 01:24:20 2023 +0000
feat port: Algebra.FreeModule.Determinant (#3767)
commit c577bee1ea0537d6a4488ad569f3252ed2123784
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed May 3 01:24:19 2023 +0000
feat: port Data.Complex.Determinant (#3765)
commit c89277f05e074a327f79381c14d659b05e68168b
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed May 3 01:24:17 2023 +0000
feat: port Analysis.SpecialFunctions.Trigonometric.Chebyshev (#3764)
commit 1dac593b7e1c149c4d234973754b4347de968595
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed May 3 01:24:16 2023 +0000
feat: port Analysis.Convex.Complex (#3763)
commit efb20cbedfb68cb1b2967449ef92b374c0f9724b
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed May 3 01:24:16 2023 +0000
feat: port Data.Matrix.Rank (#3762)
commit a65601d186c742e05cece1797b1046322f8f16f4
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Wed May 3 01:24:14 2023 +0000
feat: port CategoryTheory.Category.Groupoid (#3761)
commit 4ddf8c7c266db2c9486475955bfb75a6ccafc360
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Wed May 3 01:24:13 2023 +0000
chore: tweak `subsingleton_of_trichotomous_of_irrefl` (#3749)
Match https://github.com/leanprover-community/mathlib/pull/18749
commit 94cd04e32c71f1a64c15e6aee06eabaa6c059fb4
Author: Scott Morrison <scott@tqft.net>
Date: Tue May 2 22:58:39 2023 +0000
feat: better display of partial results from library_search (#3743)
On @PatrickMassot's [example](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20regression/near/353375130):
```lean
import Mathlib.Topology.Instances.Real
import Mathlib.Topology.Algebra.Order.Compact
import Mathlib.Tactic.LibrarySearch
example (f : ℝ → ℝ) {K : Set ℝ} (hK: IsCompact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y := by
library_search
```
we have:
* `refine IsCompact.exists_forall_le hK ?_ ?_` as one of the suggested solutions
* in fact, as the first solution (on the basis that it uses more local hypotheses than alternatives)
* none of the spurious results which use `False.elim ?_`
* and better display of the result, with hints:
```lean
refine IsCompact.exists_forall_le hK ?_ ?_
-- Remaining subgoals:
-- ⊢ Set.Nonempty K
-- ⊢ ContinuousOn (fun x ↦ f x) K
```
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit 391cddce21029cb45a255a2ab063c7d3b98b4b60
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Tue May 2 16:51:37 2023 +0000
feat: port Topology.Algebra.Module.Determinant (#3766)
commit fed5a971cac804f30a3b4b2550bc532e0b1adbaf
Author: Scott Morrison <scott@tqft.net>
Date: Tue May 2 14:49:42 2023 +0000
fix: don't look too hard for binders when indexing lemmas for library_search (#3724)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit 3f6f6282cc137af13d6c480744e58dedca712c1e
Author: Scott Morrison <scott@tqft.net>
Date: Tue May 2 12:23:16 2023 +0000
fix: linarith variable shadowing bug (#3760)
As reported on [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20bug).
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit 92a23d50515de9ac1baf29a66826ee77305b2b91
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Tue May 2 10:23:03 2023 +0000
feat: port CategoryTheory.Monoidal.Tor (#3754)
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
commit 179b81ee4cadef2f601e1f1265d266ea0cf91cd7
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Tue May 2 10:23:02 2023 +0000
Revert "feat: port Algebra.Order.ToIntervalMod (#2148)" (#3388)
This reverts commit 2d0dd3902a4a796d8f38778fec991ab1d4c2a660.
The porting comments say "Would be nice to finish leanprover-community/mathlib#17743 first". The commit message says "Might be best to wait".
We should wait; there is no urgency to merge this, and no discussion took place that argued against waiting.
commit 3f6b46f277537242649fa82a62efddb09fc8dfea
Author: Pol_tta <reddeloostw@gmail.com>
Date: Tue May 2 10:05:14 2023 +0000
feat: port LinearAlgebra.Determinant (#3694)
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit 8d401bd92990dec5d9d1aa59094789f607caf2d0
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Tue May 2 07:59:21 2023 +0000
feat: port Data.Complex.Module (#3737)
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit 0227fbbc71c1ce40bb9338c52058d0a34565653c
Author: Alex J Best <alex.j.best@gmail.com>
Date: Mon May 1 22:19:23 2023 +0000
chore: update workflows to avoid deprecation (#3755)
Forward port of https://github.com/leanprover-community/mathlib/pull/18761 - https://github.com/leanprover-community/mathlib/pull/18765 but a bit simpler as we dont have as many things set up yet.
commit 6d40a326339dc6b42c3ed25a607bb5bfe035bc7f
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Mon May 1 22:19:22 2023 +0000
feat: port CategoryTheory.Functor.LeftDerived (#3751)
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit e57a8f962faca1a6949a74daec03e5b350995af8
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Mon May 1 22:19:21 2023 +0000
feat: port CategoryTheory.Sites.LeftExact (#3706)
commit fc3894f2f75c7b860783e8a90fd767bcb00b2cb9
Author: Pol_tta <pol_tta@outlook.jp>
Date: Mon May 1 22:19:20 2023 +0000
feat: make `Acc.rec` and many related defs computable (#3535)
Lean 4 code generator has had no native supports for `Acc.rec`.
This PR makes `Acc.rec` computable.
This change makes many defs computable. Especially, computable `PFun.fix` and `Part.hasFix` enables us to reason about `partial` functions.
This PR also renames some instances and gives `PFun.lift` `@[coe]` attr.
commit eb1f66662c488bafde47edd140eef4a47bc59d2a
Author: Bulhwi Cha <chabulhwi@semmalgil.com>
Date: Mon May 1 22:02:09 2023 +0000
refactor: delete `import` line (#3745)
Delete an unnecessary `import` line.
commit 28ae9843458339c54de11f62fce84002528759af
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Mon May 1 20:06:10 2023 +0000
feat: port CategoryTheory.Preadditive.ProjectiveResolution (#3740)
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
commit 52e6ad71693190465481e0ae20d97913dbba06e9
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Mon May 1 17:47:55 2023 +0000
chore: Move lattice `finset` lemmas around (#3748)
Match https://github.com/leanprover-community/mathlib/pull/18900
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit 5b940a6dc1a1bd5f2f4a6f271059bbea0e3857bc
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Mon May 1 17:47:54 2023 +0000
feat: port CategoryTheory.Abelian.Exact (#3638)
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
commit 0ea443f63e211696d5a166c82f7469cc2cdc1d82
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Mon May 1 15:10:19 2023 +0000
feat: `f.update i '' Icc a b = Icc (f.update i a) (f.update i b)` (#3747)
Match https://github.com/leanprover-community/mathlib/pull/18892
* [`order.lattice`@`d6aad9528ddcac270ed35c6f7b5f1d8af25341d6`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/order/lattice?range=d6aad9528ddcac270ed35c6f7b5f1d8af25341d6..e4bc74cbaf429d706cb9140902f7ca6c431e75a4)
* [`algebra.group.pi`@`90df25ded755a2cf9651ea850d1abe429b1e4eb1`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=90df25ded755a2cf9651ea850d1abe429b1e4eb1..e4bc74cbaf429d706cb9140902f7ca6c431e75a4)
* [`data.set.intervals.pi`@`4020ddee5b4580a409bfda7d2f42726ce86ae674`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/intervals/pi?range=4020ddee5b4580a409bfda7d2f42726ce86ae674..e4bc74cbaf429d706cb9140902f7ca6c431e75a4)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit e95cccde5645c855b0c08a5fb4d944adf442a4b7
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Mon May 1 13:19:51 2023 +0000
feat: port Topology.Category.Profinite.Projective (#3746)
commit 55637dc9d43c30243cb0d8578cabcabf4dedbc8c
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Mon May 1 11:02:54 2023 +0000
feat: port Mathlib.Data.Ordmap.Ordnode (#1455)
Co-authored-by: Arien Malec <arien.malec@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
commit 64d186af31d440f3743d6862c0f39cf553fcdca1
Author: Violeta Hernández <vi.hdz.p@gmail.com>
Date: Mon May 1 08:43:35 2023 +0000
feat: port ZFC set intersection (#3345)
Also fixes some erroneous theorem names from the port.
[`set_theory.zfc.basic`@`98bbc3526516bca903bff09ea10c4206bf079e6b`..`f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a`](https://leanprover-community.github.io/mathlib-port-status/file/set_theory/zfc/basic?range=98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a)
Mathlib 3: https://github.com/leanprover-community/mathlib/pull/18232
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
commit 5925a364a984ab06f0d1b425339c4bb5cd1b2646
Author: Scott Morrison <scott@tqft.net>
Date: Mon May 1 01:58:20 2023 +0000
feat: port Topology.Category.Profinite.Basic (#3705)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>
commit c272f4940037d117009ce720b7aba0bad3986627
Author: Alex J Best <alex.j.best@gmail.com>
Date: Mon May 1 01:36:18 2023 +0000
feat: annotate build errors in the github files changed tab using an action (#3739)
This is suboptimal as it doesn't handle multiline comments, but it is better than nothing, and the implementation works out of the box. This is broadly similar to the support we had in mathlib 3, but the implementation is different as we no longer have json errors as an option, so must instead match an errorformat directly (the gcc one works fine).
Supporting multiline error messages appears not to be possible using the builtin output without further processing with the current state of problem matchers supported by github (which follow the vscode design).
Thus to get an improvement on this the build output must be piped through a second program that processes it in some way, or a lake build type command should be added that outputs in a required format.
Likewise to get annotations for linter failures we will need to add extra information to the linter output, either setting the annotations ourselves (as we did in mathlib 3) or at least adding line numbers to the existing output so that we can at least match it with a problem matcher again.
commit 77416707240d45fb64906bc8f7f28d6f29cfda2b
Author: Bulhwi Cha <chabulhwi@semmalgil.com>
Date: Sun Apr 30 23:31:19 2023 +0000
chore: move theorems on `String` to std4 (#3712)
https://github.com/leanprover/std4/pull/124 moves the following from Mathlib4 to Std4:
* helper `simp` theorems on `String.Pos`
* `String.utf8GetAux.inductionOn`
commit 6a64ec0b0f5ee12b611215ac7ad1e0145465a327
Author: Ruben Van de Velde <reddeloostw@gmail.com>
Date: Sun Apr 30 11:38:03 2023 +0000
feat: port FieldTheory.Tower (#3716)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
commit 76707255936de099ae6835e7ddbe5f7bf95a7a36
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Sat Apr 29 23:07:53 2023 +0000
feat: port Algebra.Category.Group.ZModuleEquivalence (#3732)
commit 543b8ec1ea21d7a3321234bb0b6532576a897c61
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Sat Apr 29 23:07:52 2023 +0000
feat: port AlgebraicTopology.ExtraDegeneracy (#3729)
commit eb11681ef13f0d1aba2ff267a20bd08883484f82
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Sat Apr 29 22:52:42 2023 +0000
feat: port CategoryTheory.Monad.Coequalizer (#3733)
commit 6a28eee3a21942016a01bbada70ce9a6a40ba8e5
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Sat Apr 29 22:28:56 2023 +0000
chore: no newline before aligns (#3735)
Co-authored-by: Moritz Firsching <firsching@google.com>
commit a7e9e4ab120a3b6d10251d3c3d24a1e60c13dca8
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Sat Apr 29 16:26:38 2023 +0000
feat: `a * b ≠ b ↔ a ≠ 1` (#3726)
https://github.com/leanprover-community/mathlib/pull/18635
* [`algebra.group.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..84771a9f5f0bd5e5d6218811556508ddf476dcbd)
* [`algebra.order.field.basic`@`44e29dbcff83ba7114a464d592b8c3743987c1e5`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/field/basic?range=44e29dbcff83ba7114a464d592b8c3743987c1e5..84771a9f5f0bd5e5d6218811556508ddf476dcbd)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit dc012f816b787bcb80007f2bc1b5e6604aa57b28
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Sat Apr 29 13:32:59 2023 +0000
feat: port LinearAlgebra.ProjectiveSpace.Independence (#3728)
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
commit 8dd639e1083340aed6138d8ad7f954091b037267
Author: Scott Morrison <scott@tqft.net>
Date: Sat Apr 29 13:32:58 2023 +0000
fix: find MathlibExtras from downstream projects (#3721)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit 73bab6a59163675f3f1f26530bac9c2571eba84b
Author: Scott Morrison <scott@tqft.net>
Date: Sat Apr 29 13:32:57 2023 +0000
fix: allow library_search to run when maxHeartbeats = 0 (#3720)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit 301ea2db46c56d28eb73f418ab992b0010e5f75d
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Sat Apr 29 13:32:56 2023 +0000
chore: Remove `finset.sup_finset_image` (#3713)
Match https://github.com/leanprover-community/mathlib/pull/18893
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
commit f667fdec730173011b40f4dcea8c79c33eed39b6
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Sat Apr 29 13:32:55 2023 +0000
feat: port CategoryTheory.Abelian.Transfer (#3424)
commit 029b212612c336f75d26163cebd5e129a455847e
Author: Alex J Best <alex.j.best@gmail.com>
Date: Sat Apr 29 10:38:07 2023 +0000
feat: allow several tactics on types that are slightly less obviously Types (#3682)
Many tactics attempt to get the universe of the sort of the terms involved by matching on the level being a succ of something.
Unfortunately this fails on some nontrivial examples like mvpolynomial which can have type `Sort (max (u+1) (v+1))`
Instead we decrement the level manually after matching it.
See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60ring.60.20tactic.20cannot.20prove.20equality.20about.20.60MvPolynomial.60/near/352549549
This PR modifies ring, ring_nf, nontriviality, polyrith, linarith, and some norm_num handlers to appropriately handle this.
Test cases showing examples that failed before (inspired by the case of mvpolynomial, but in principle there could be other interesting types that have multiple universe parameters in this way, some of which may even have a linear order who knows).
In doing so we factor out `inferTypeQ'` into its own file `Mathlib.Tactic.Qq` for mathlib-relevant extensions of Qq
commit a540fe1433f247fd5cd6561401ab813cf04a5e9e
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Sat Apr 29 09:57:49 2023 +0000
feat: port LinearAlgebra.ProjectiveSpace.Basic (#3692)
commit d2c96a57df11efb8eec9f31377e5de800012433c
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Sat Apr 29 05:39:03 2023 +0000
chore: add hash for Data.MvPolynomial.Polynomial (#3723)
commit 288a7d79cf1b6dfd4940082700efa5b8dc15d496
Author: Jason Yuen <jason_yuen2007@hotmail.com>
Date: Sat Apr 29 03:33:44 2023 +0000
feat: port LinearAlgebra.SymplecticGroup (#3696)
commit 3230cdeee0ab5da8fc47680e4d5da87addcc90e7
Author: Alex J Best <alex.j.best@gmail.com>
Date: Fri Apr 28 23:45:34 2023 +0000
feat: make alias compile code when possible (#3719)
commit 36844e9cb778e4e857c8c9b0b0339c876679f4a8
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Apr 28 23:45:32 2023 +0000
chore: forward-port leanprover-community/mathlib#18880 (#3717)
commit 24f74e319f706f55aef284703cddec753ffadb62
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Fri Apr 28 23:19:17 2023 +0000
chore: Rename to `AddLocalization` (#3714)
This name wasn't properly capitalised.
commit aaf828ddcf36204db88d6e02fa5a90da2126a1bb
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Apr 28 21:59:08 2023 +0000
chore: update SHA (#3711)
I forgot to update the SHA in #3675
commit b50e5c5aa89de2b79df485083b3f5c1bb00b4b8d
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Fri Apr 28 21:59:07 2023 +0000
feat: port LinearAlgebra.Matrix.Diagonal (#3695)
Some proofs in the last section were failing even with eta-experiment, so I generalized some lemmas from `Field`s to `Semifield`s.
commit f5f2fbf04d6c9b0a995807c408ade9e71bad05f1
Author: Adam Topaz <github@adamtopaz.com>
Date: Fri Apr 28 18:56:37 2023 +0000
feat: Port Topology.Category.CompHaus.Projective (#3715)
commit 863aebc8ccf10ff0c19a25fad7344e8a585c9108
Author: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Date: Fri Apr 28 17:46:02 2023 +0000
feat LinearAlgebra.Basis: add basis.restrictScalars (#3707)
Mathlib4 version of https://github.com/leanprover-community/mathlib/pull/18814
[`linear_algebra.basis`@`2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e`..`04cdee31e196e30f507e8e9eb2d06e02c9ff6310`](https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/basis?range=2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e..04cdee31e196e30f507e8e9eb2d06e02c9ff6310))
commit a585b6ffc2dc1351ab8a5aa1534c26f22c2d7910
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Fri Apr 28 14:30:45 2023 +0000
feat: Lemmas relating definitions of infinite sets (#3672)
Match https://github.com/leanprover-community/mathlib/pull/18620
* [`data.set.finite`@`c941bb9426d62e266612b6d99e6c9fc93e7a1d07`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/finite?range=c941bb9426d62e266612b6d99e6c9fc93e7a1d07..52fa514ec337dd970d71d8de8d0fd68b455a1e54)
* [`data.finset.locally_finite`@`f24cc2891c0e328f0ee8c57387103aa462c44b5e`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/locally_finite?range=f24cc2891c0e328f0ee8c57387103aa462c44b5e..52fa514ec337dd970d71d8de8d0fd68b455a1e54)
* [`data.nat.lattice`@`2445c98ae4b87eabebdde552593519b9b6dc350c`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/lattice?range=2445c98ae4b87eabebdde552593519b9b6dc350c..52fa514ec337dd970d71d8de8d0fd68b455a1e54)
commit 601c82017f39b855b6a697a78d4a244b668996e7
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Fri Apr 28 14:00:44 2023 +0000
feat: port LinearAlgebra.Matrix.Transvection (#3700)
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
commit 3d576486048be2cbae503d1c1e7f5a0a85b66a6c
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Fri Apr 28 11:44:00 2023 +0000
feat: For any `b`, there exists a set `s` of independent atoms such that `Sup s` is the complement of `b` (#3588)
Match https://github.com/leanprover-community/mathlib/pull/8475
* [`order.compactly_generated`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`e8cf0cfec5fcab9baf46dc17d30c5e22048468be`](https://leanprover-community.github.io/mathlib-port-status/file/order/compactly_generated?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..e8cf0cfec5fcab9baf46dc17d30c5e22048468be)
* [`order.directed`@`485b24ed47b1b7978d38a1e445158c6224c3f42c`..`e8cf0cfec5fcab9baf46dc17d30c5e22048468be`](https://leanprover-community.github.io/mathlib-port-status/file/order/directed?range=485b24ed47b1b7978d38a1e445158c6224c3f42c..e8cf0cfec5fcab9baf46dc17d30c5e22048468be)
commit d3e6edfe83effc9316d710b3e4421b16162e73d1
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Fri Apr 28 11:10:45 2023 +0000
feat: port CategoryTheory.Action (#3657)
commit bc85faaf38cdda2b9c3f808ba563c232f5f815a0
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Fri Apr 28 11:10:44 2023 +0000
feat: port CategoryTheory.Preadditive.Projective (#3615)
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit b98b04707b0c77941e61f598a4b8c8164a2c2482
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Fri Apr 28 10:54:06 2023 +0000
feat: port LinearAlgebra.Matrix.ZPow (#3671)
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
commit cd980733e0e92568cb77dbb4a9c0f6b3498dc9ce
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Fri Apr 28 09:49:14 2023 +0000
feat: port LinearAlgebra.Matrix.FiniteDimensional (#3698)
commit 740bbec09993a7a71a993aaf7fdee3571005215c
Author: Bulhwi Cha <chabulhwi@semmalgil.com>
Date: Fri Apr 28 09:32:10 2023 +0000
refactor: change arguments order (#3701)
Change the order of the arguments to `String.utf8GetAux.add_right_cancel`.
commit 4d1c8e0454e1470c3cbc8e3aa41d5745acd1cdc1
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Fri Apr 28 06:56:28 2023 +0000
feat: port LinearAlgebra.Matrix.InvariantBasisNumber (#3697)
commit 15d98e6b55a610e11d16e02aca4fc7be760c5ffd
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Fri Apr 28 06:56:27 2023 +0000
feat: port AlgebraicTopology.Nerve (#3693)
commit e35da366b8e442a61e77516edd8197e8715264b5
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Apr 28 06:56:26 2023 +0000
forward-port leanprover-community/mathlib#18840 (#3678)
commit d456dd3ce4146aa82e05ac02aae437901b534fc1
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Apr 28 06:56:25 2023 +0000
chore: forward-port leanprover-community/mathlib#18802 (#3677)
commit e234e1dbab60d5cb2491ee19f608fe6357d7244c
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Apr 28 06:56:24 2023 +0000
chore: forward-port leanprover-community/mathlib#18869 (#3676)
commit bd1736fa511c00b8607b3e1134213cd963b923c1
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Apr 28 06:56:23 2023 +0000
chore: forward-port leanprover-community/mathlib#18842 (#3675)
commit 7d4f125478272f478180c413365372d3069e8a63
Author: Yaël Dillies <yael.dillies@gmail.com>
Date: Fri Apr 28 06:56:22 2023 +0000
feat: The equivalence between `fin n → fin m` and `fin (m ^ n)` (#3673)
Match https://github.com/leanprover-community/mathlib/pull/14817
[`algebra.big_operators.fin`@`f93c11933efbc3c2f0299e47b8ff83e9b539cbf6`..`cdb01be3c499930fd29be05dce960f4d8d201c54`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/big_operators/fin?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..cdb01be3c499930fd29be05dce960f4d8d201c54)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit 535bb666094594a96afc3f425fe1c5cd49261836
Author: Eric Wieser <wieser.eric@gmail.com>
Date: Fri Apr 28 06:56:21 2023 +0000
chore: forward-port leanprover-community/mathlib#18833 (#3660)
The previously hacky proofs with porting notes can be discarded in favor of the ones from mathport.
commit 7f09ac6a714e33333682d4f6ff7c95bac10684d2
Author: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri Apr 28 06:56:19 2023 +0000
perf: improve performance of `to_additive` (#3632)
* `applyReplacementFun` now treats applications `f x_1 ... x_n` as atomic, and recurses directly into `f` and `x_i` (before it recursed on the partial appliations `f x_1 ... x_j`)
* I had to reimplement the way `to_additive` reorders arguments, so at the same time I also made it more flexible. We can now reorder with an arbitrary permutation, and you have to specify this by providing a permutation using cycle notation (e.g. `(reorder := 1 2 3, 8 9)` means we're permuting the first three arguments and swapping arguments 8 and 9). This implements the first item of #1074.
* `additiveTest` now memorizes the test on previously-visited subexpressions. Thanks to @kmill for this suggestion!
The performance on (one of) the slowest declaration(s) to additivize (`MonoidLocalization.lift`) is summarized below (note: `dsimp only` refers to adding a single `dsimp only` tactic in the declaration, which was done in #3580)
```
original: 27400ms
better applyReplacementFun: 1550ms
better applyReplacementFun + better additiveTest: 176ms
dsimp only: 6710ms
better applyReplacementFun + dsimp only: 425ms
better applyReplacementFun + better additiveTest + dsimp only: 128ms
```
commit ccfc417d5df188a52936f4722ab1162a22b9e162
Author: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Fri Apr 28 05:58:44 2023 +0000
feat: port LinearAlgebra.Matrix.Basis (#3691)
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Johan Commelin <johan@commelin.net>
commit 6fc9d5e9d711f3812bbd7cd0fbeb2fed11cf9c6e
Author: Jeremy Tan Jie Rui <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Fri Apr 28 05:41:51 2023 +0000
feat: port LinearAlgebra.FreeModule.Finite.Matrix (#3690)
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
commit 7b0b99d0366fcca78f849aaef42e8dcd0975ed66
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Fri Apr 28 03:54:51 2023 +0000
feat: port LinearAlgebra.Matrix.ToLin (#3552)
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit 4f6380966f207897ef1487010c80d15f24769971
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Fri Apr 28 02:53:49 2023 +0000
feat: port AlgebraicTopology.SimplicialSet (#3689)
commit 7b88b65bd51282f240fc40b1bd6c1e7d8c227be6
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Fri Apr 28 02:53:48 2023 +0000
ci: lint references.bib (#3683)
Ported from mathlib3.
commit b8ad9541c1a9fb132cad12283b3accc56c5ed35e
Author: Moritz Firsching <moritz.firsching@gmail.com>
Date: Fri Apr 28 02:53:47 2023 +0000
chore: rename Zpowers -> ZPowers (#3681)
Co-authored-by: Moritz Firsching <firsching@google.com>
commit eb417549e64541742039abd0dc9b823388124907
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Fri Apr 28 02:33:14 2023 +0000
feat: port Topology.Algebra.Module.Multilinear (#3348)
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: ADedecker <anatolededecker@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit fe28ed480a44857c878f429eabc66b9fee4f3a45
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Fri Apr 28 01:23:38 2023 +0000
feat: port Topology.Algebra.Module.StrongTopology (#3684)
Co-authored-by: ADedecker <anatolededecker@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
commit 1113f1cefa6387fb404087427f48596810d95acb
Author: Henrik Böving <hargonix@gmail.com>
Date: Fri Apr 28 00:11:16 2023 +0000
fix: mathlib4_docs cleanup routine (#3631)
commit ed822e7be3f58018b6fd816b957fd888db4b35c2
Author: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Thu Apr 27 23:33:25 2023 +0000
feat : port CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (#3605)
This was harder than it looked (the proofs are long and broke).
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
commit 78d77dfbcae2747913005e50dad80692cb1ff940
Author: Adam Topaz <github@adamtopaz.com>
Date: Thu Apr 27 23:18:23 2023 +0000
feat: Port Topology.Category.CompHaus.Basic (#3688)
Relatively straightforward port.
Co-authored-by: Scott Morrison <scott@tqft.net>
commit d1a1c6b104967ffed8ca69ebb4f3ea9a4eb25424
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Thu Apr 27 21:43:33 2023 +0000
feat: port Analysis.Convex.StoneSeparation (#3686)
commit 2f36c58966790d0a91aaa910836751e289259f12
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Thu Apr 27 21:43:32 2023 +0000
feat: port CategoryTheory.Noetherian (#3685)
commit aaa5e0a421c8b53d60e6b7d1341ade2d5b2e59b3
Author: Felix-Weilacher <fweilach@andrew.cmu.edu>
Date: Thu Apr 27 21:26:10 2023 +0000
chore: forward port leanprover-community/mathlib#18864 (#3687)
Forward port changes from leanprover-community/mathlib#18864 to Topology/Perfect.lean and MeasureTheory/MeasurableSpace.lean
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
commit 2dab08df0323c6e58ace9b611c7e951602d0a2c0
Author: Joël Riou <joel.riou@universite-paris-saclay.fr>
Date: Thu Apr 27 15:27:17 2023 +0000
feat: port CategoryTheory.Sites.Adjunction (#3663)
commit c934e5d186bdc16bb6f0b181e3ebe1e95acbe333
Author: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Date: Thu Apr 27 14:06:46 2023 +0000
chore: forward-port generalisation (#3679)
* [`data.finsupp.basic`@`2651125b48fc5c170ab1111afd0817c903b1fc6c`..`57911c5a05a1b040598e1e1…
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Also fixes some erroneous theorem names from the port.
set_theory.zfc.basic@98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1aMathlib 3: leanprover-community/mathlib3#18232
sInter_coemathlib3#18773