[Merged by Bors] - chore(Turan): remove superfluous DecidableEq assumption #15280
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
Found by the DecidableEq linter in #10235.
grunweg
added
the
easy
PR summary 74320a91fdImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit> |
grunweg
added a commit
that referenced
this pull request
Jul 30, 2024
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Aug 1, 2024
Found by the DecidableEq linter in #10235. Co-authored-by: Parcly Taxel <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Rida-Hamadani
added a commit
that referenced
this pull request
Aug 3, 2024
commit 484c019b766dc78afa7c381bb71a66268b10af84 Author: sgouezel <[email protected]> Date: Sat Aug 3 10:01:55 2024 +0000 chore: remove some uses of `open Classical`, part 2 (#15413) See #15371. commit 321e94eabbb5e264d2302c0b0e3f72c498a085a2 Author: grunweg <[email protected]> Date: Sat Aug 3 09:06:17 2024 +0000 doc: tweak documention of the longLine linter (#15458) commit eaef110731047b8c61e3185879fe1e5a64bfdfad Author: Peter Nelson <[email protected]> Date: Sat Aug 3 02:06:31 2024 +0000 feat(Data/Set/Finite): union of infinitely many sets is infinite (#15447) We add three separate versions of the statement that the union of an infinite collection of sets is infinite. commit 2f5275c40a06f08f833fce34523c6820cd10ff4e Author: JonBannon <[email protected]> Date: Fri Aug 2 21:35:03 2024 +0000 feat: `RCLike` versions of Hahn-Banach separation theorems (#15416) Generalized first definition in `Mathlib.Analysis.NormedSpace.Extend`, and used this to prove `RCLike` generalizations of Hahn-Banach separation theorems. Co-authored-by: Jireh Loreaux <[email protected]> Co-authored-by: JonBannon <[email protected]> commit 9756867d21c64a4e91b7e484f3b4cf8262c1897d Author: Andrew Yang <[email protected]> Date: Fri Aug 2 19:53:57 2024 +0000 feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts (#14428) Co-authored-by: Andrew Yang <[email protected]> commit 7669be18c4affa2e4909d4edc9d3c81c03d5e3ed Author: james18lpc <[email protected]> Date: Fri Aug 2 14:42:18 2024 +0000 feat: Scalar multiplication of an indicator function (#15311) from GibbsMeasure Co-authored-by: Yael Dillies <[email protected]> commit 01959f98a3774783925316cdfa88343f49515bae Author: Sina Hazratpour <[email protected]> Date: Fri Aug 2 08:59:13 2024 +0000 feat(CategoryTheory): wide subcategories (#15374) This PR introduces the notion of wide subcategory. The API is in parallel with that of full subcategories. commit 9c39e72da5e57ab76a512007bddf308928783228 Author: grunweg <[email protected]> Date: Fri Aug 2 08:48:24 2024 +0000 feat: rewrite updating style-exceptions in Lean (#14697) Rewrite the `update-style-exceptions` script in Lean, by adding an --update flag to `lint_style`: in this mode, the script will remove any exceptions which are no longer needed, add new entries for any current error, and try to leave existing entries untouched. (With one exception: if a "file too long" error still applies, but the file is currently at least 200 lines shorter, we update it to the new entry.) commit 28022937e4162e38193d61080c1d409776f6f1f7 Author: Stefan Kebekus <[email protected]> Date: Fri Aug 2 08:25:29 2024 +0000 Fix documentation (#15435) docs: fix typo in the documentation commit 6d1096a18aae512f5ae18ecefe0b67292535aea3 Author: Kim Morrison <[email protected]> Date: Fri Aug 2 07:08:50 2024 +0000 chore: backports for leanprover/lean4#4814 (part 13) (#15397) see https://github.com/leanprover-community/mathlib4/pull/15245 Co-authored-by: Ruben Van de Velde <[email protected]> commit 5e31476b7bd5a4e7be6793865c534824260ff3e6 Author: Dagur Asgeirsson <[email protected]> Date: Fri Aug 2 07:08:49 2024 +0000 fix(CategoryTheory): move a general lemma about created limits to the correct file (#15264) This lemma was accidentally in a file about light profinite sets, but is a completely general category-theoretic statement. commit b941d5eafd255cdeb8906de5be4a147f4ab4da6c Author: Kim Morrison <[email protected]> Date: Fri Aug 2 06:24:05 2024 +0000 chore: backports for leanprover/lean4#4814 (part 12) (#15396) see https://github.com/leanprover-community/mathlib4/pull/15245 commit 35ccd78e25895200656760dd478f0ad21c6f9046 Author: grunweg <[email protected]> Date: Thu Aug 1 22:59:42 2024 +0000 fix(lint-style): mention the correct size limit in 'file too long' errors (#15414) The previous error message (for github consumption) was wrong in two ways: - it would always print the size limit, even when there was no previous exception for this file - it would print the *new* limit, not the previous one To fix this, we need to make an existing limit part of the error data. commit 246247f72011e56c8d1740763f0b070b1471f067 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Aug 1 21:35:56 2024 +0000 chore: update Mathlib dependencies 2024-08-01 (#15405) This PR updates the Mathlib dependencies. commit e318dc809621d361138729ac645cdecb5598479b Author: Dagur Asgeirsson <[email protected]> Date: Thu Aug 1 20:50:36 2024 +0000 refactor(Condensed): merge files about discreteness (#15402) commit adcc6aa472faff7d33c3b30df32c8bb3f1b04e10 Author: Yury G. Kudryashov <[email protected]> Date: Thu Aug 1 20:21:09 2024 +0000 feat(Topology/ENNReal): `zpow` is continuous (#15381) Also add some `fun_prop` attrs commit dea069eab3f351403ca99fb4bb4ee2e37ed235f3 Author: grunweg <[email protected]> Date: Thu Aug 1 19:38:46 2024 +0000 chore(Turan): remove superfluous DecidableEq assumption (#15280) Found by the DecidableEq linter in #10235. Co-authored-by: Parcly Taxel <[email protected]> commit cde759037381ecec1fede8bbe2e251498b1fb635 Author: grunweg <[email protected]> Date: Thu Aug 1 19:15:26 2024 +0000 chore: three more Fintype -> Finite replacements (#15283) Found by the linter in #10235. commit 852c1ad8be5a7ea86187ef929ae0b18feb9cf3eb Author: james18lpc <[email protected]> Date: Thu Aug 1 17:52:43 2024 +0000 feat: notations to specify sigma algebras for integrability, measures and kernels (#15316) from GibbsMeasure Co-authored-by: Yael Dillies <[email protected]> commit f2107dde92dd94c4ec70f233ee60cad65e1dc126 Author: Ruben Van de Velde <[email protected]> Date: Thu Aug 1 17:52:42 2024 +0000 fix: generalize AlgEquiv.coe_mk (#15243) commit 3f10dd7509e3e1bcaaf619d5cac7cd58f394d263 Author: grunweg <[email protected]> Date: Thu Aug 1 17:52:41 2024 +0000 chore: remove Data/Buffer/Basic (#15241) This was an empty placeholder created for the porting dashboard: we can remove it now. commit f05779eb6777b088f517532b34c90a48b16e58ee Author: Kim Morrison <[email protected]> Date: Thu Aug 1 16:59:35 2024 +0000 chore: remove unnecessary implicit arguments in MonoidWithZeroHom.coe_copy (#15248) It's perfectly fine for these to just be instance implicit arguments. commit 45697ceb014421d7d0db482d76288097b6c784b7 Author: Kim Morrison <[email protected]> Date: Thu Aug 1 16:02:41 2024 +0000 chore: backports for leanprover/lean4#4814 (part 11) (#15394) see https://github.com/leanprover-community/mathlib4/pull/15245 commit 786a0509b7bb229c6bc7dae0cac0cd090bb03132 Author: Kim Morrison <[email protected]> Date: Thu Aug 1 16:02:40 2024 +0000 chore: backports for leanprover/lean4#4814 (part 9) (#15389) see https://github.com/leanprover-community/mathlib4/pull/15245 commit a33cf03c4f57826d8dcb653483916aaeb0b55e65 Author: Jireh Loreaux <[email protected]> Date: Thu Aug 1 15:33:58 2024 +0000 feat: `StarModule ℝ E` implies `StarModule ℝ≥0 E` (#15392) commit 19f233e7bbffce214c7b8df1f1a693958c243c77 Author: Adam Topaz <[email protected]> Date: Thu Aug 1 14:36:47 2024 +0000 feat: Adds a variant of lemma about eigenvectors. (#15404) commit 227496b051547e76b4f5e365b8824cc6f5663ff3 Author: grunweg <[email protected]> Date: Thu Aug 1 14:36:45 2024 +0000 chore: avoid yoda comparisons (#15399) As recommended in the Lean 4.10 release blog, prefer comparisons `(· == a)` over `(a == ·)`. commit 4410f363ebb18b731b98727a3d39d1b6e36ae17c Author: james18lpc <[email protected]> Date: Thu Aug 1 14:36:44 2024 +0000 feat: `gcongr` with `Finset.coe_subset` (#15312) from GibbsMeasure Co-authored-by: Yael Dillies <[email protected]> commit bc5f69ee17d8a4dc8b38f9b29c4529ed716a075c Author: grunweg <[email protected]> Date: Thu Aug 1 14:36:43 2024 +0000 doc(Tactic/HelpCmd): fix typo (option -> attribute) (#15307) commit 1308f9597e6fc966db1271e227149fa7db7cbdc1 Author: Yaël Dillies <[email protected]> Date: Thu Aug 1 13:36:39 2024 +0000 feat: Upper bound on multinomial coefficients with even exponent (#15338) From LeanAPAP Co-authored-by: Bhavik Mehta <[email protected]> commit 0139a899fdb48caffb0277abf97006b8dace569e Author: Yury G. Kudryashov <[email protected]> Date: Thu Aug 1 10:24:04 2024 +0000 feat(IntermediateValue): add `IsFixedPt` corollaries (#15395) Motivated by https://github.com/b-mehta/sharkovsky Also move the definition of `Function.IsFixedPt` to `Logic/Function/Defs`. commit 2df7d9446f22706562263d8b55076dc073e10d02 Author: Kim Morrison <[email protected]> Date: Thu Aug 1 09:23:33 2024 +0000 chore: backports for leanprover/lean4#4814 (part 10) (#15390) see https://github.com/leanprover-community/mathlib4/pull/15245 commit 8de1883595f6ca9e21fc87facf20da344267a8b3 Author: Etienne <[email protected]> Date: Thu Aug 1 09:13:24 2024 +0000 feat(Topology): add API for compactly generated spaces (#15203) Define compactly generated topological spaces, which are spaces whose topology is coinduced by continuous maps whose domain is compact Hausdorff. Prove basic properties and instances. Provide instances for sequential spaces and Hausdorff weakly locally compact spaces. Co-authored-by: Etienne <[email protected]> commit 26269fbbf15d1678546f00c1096c7b4b2ab38446 Author: Dagur Asgeirsson <[email protected]> Date: Thu Aug 1 08:35:57 2024 +0000 refactor(Topology/Category): unify some definitions of subcategories of compact Hausdorff spaces (#12930) This PR unifies the definitions of the categories `CompHaus`, `Profinite`, `Stonean`, and `LightProfinite` by defining a structure `CompHausLike P` depending on a predicate `P` on topological spaces. Many of the properties of these categories of compact Hausdorff spaces are shared between them and this approach reduces duplication of boilerplate code, in particular the explicit constructions of certain limits and colimits. commit d37ebdd7ac7a2a5790ad25a88628580394956d78 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Aug 1 08:19:11 2024 +0000 chore: update Mathlib dependencies 2024-08-01 (#15393) This PR updates the Mathlib dependencies. commit b2d7c49b234d7ec1cb38ffdfc21e345e240039e2 Author: Yury G. Kudryashov <[email protected]> Date: Thu Aug 1 08:01:45 2024 +0000 chore(MeasureTheory/Prod): minor golf, add a docstring (#15353) commit 180c2e011eb6d45d282c114aeda47cab58f02ba2 Author: Kim Morrison <[email protected]> Date: Thu Aug 1 07:51:36 2024 +0000 chore: report commits in nightly testing bot (#15145) commit c96401c7496392a2200dc78c0b334df0561466dc Author: Dagur Asgeirsson <[email protected]> Date: Thu Aug 1 04:29:16 2024 +0000 refactor(Topology/Category): use `CompHausLike` API for limits in `Profinite` and `Stonean` (#15363) commit 81a4038d73cc805509dc59484fd1ac01e262f291 Author: Jireh Loreaux <[email protected]> Date: Thu Aug 1 04:08:26 2024 +0000 refactor: remove some dependence on `circle` in C⋆-algebras (#15343) commit a8a6183c88b4201ffbcd41571b31d1e2a80400c3 Author: Frédéric Dupuis <[email protected]> Date: Thu Aug 1 03:42:29 2024 +0000 feat(CstarAlgebra): define Hilbert C⋆-modules (#15244) This PR defines [Hilbert C⋆-modules](https://en.wikipedia.org/wiki/Hilbert_C*-module). A Hilbert C⋆-module is a complex module `E` together with a right `A`-module structure, where `A` is a C⋆-algebra, and with an "inner product" that takes values in `A`. This inner product satisfies the Cauchy-Schwarz inequality, and induces a norm that makes `E` a normed vector space. This is a stepping stone towards proving that matrices with entries in a C⋆-algebra are a C⋆-algebra, which is in turn needed to define completely positive maps. Co-authored-by: Frédéric Dupuis <[email protected]> commit 5745d771fd134e2de175231204c36a26b66da3ad Author: Kim Morrison <[email protected]> Date: Thu Aug 1 02:49:41 2024 +0000 chore: backports for leanprover/lean4#4814 (part 8) (#15349) see https://github.com/leanprover-community/mathlib4/pull/15245 commit e76ade82288dd52fdf269abbd15a222403fa4d78 Author: Yury G. Kudryashov <[email protected]> Date: Thu Aug 1 02:03:27 2024 +0000 feat(ContinuousOn): add `ContinuousOn.iterate` (#15388) From https://github.com/b-mehta/sharkovsky/ commit 35ff6b82b6171c63f589f103711743498ea840ce Author: Yury G. Kudryashov <[email protected]> Date: Thu Aug 1 02:03:26 2024 +0000 feat(Separation): add `IsClosed.isClosed_eq` (#15382) Named similarly to `IsClosed.isClosed_le`. From https://github.com/b-mehta/sharkovsky. commit d862d98ec82be0568ea47c22f2ba3face0a76e54 Author: grunweg <[email protected]> Date: Thu Aug 1 01:16:36 2024 +0000 chore(MvPowerSeries/Basic): remove superfluous DecidableEq (#15302) Found by the linter in #10235. commit 1f6c167d6751416eae75e61ac792d3d75022c549 Author: grunweg <[email protected]> Date: Thu Aug 1 01:16:35 2024 +0000 chore(Data/Finsupp/Defs): remove superfluous DecidableEq (#15301) Found by the linter in #10235. commit 83173e418aefd5114b8427a05e9f10466cbc36b9 Author: Ruben Van de Velde <[email protected]> Date: Thu Aug 1 00:14:52 2024 +0000 chore: backport some changes for lean v4.11.0 (#15368) commit 00f0e1371ca603a77d89fadbba72962ea1ff1e9e Author: grunweg <[email protected]> Date: Thu Aug 1 00:14:51 2024 +0000 chore(DirectSum/Algebra): remove superfluous DecidableEq (#15304) Found by the linter in #10235. commit 0cafb4a8703ca8544ffa9a371c62ae89b8a72da4 Author: Kim Morrison <[email protected]> Date: Thu Aug 1 00:14:49 2024 +0000 chore: robustifying for debug.byAsSorry (part 14) (#15247) commit a904cfd0505d3ec88828db39649df408c0a286a5 Author: Kim Morrison <[email protected]> Date: Thu Aug 1 00:14:48 2024 +0000 chore: backports for leanprover/lean4#4814 (part 1) (#15245) The new variables inclusion mechanism https://github.com/leanprover/lean4/pull/4814 is going to require many changes to Mathlib. Some of these changes are to make sure typeclass hypotheses are not unnecessarily included. This is achieved either by using `section` to bound `variable [...]`, using `variable ... in`, or reordering theorems. (I think you can see all three being using here.) Other changes require adding `include ...` to include variables that the new mechanism won't automatically include. These changes can't be backported to master, and instead are accumulating on the `lean-pr-testing-4814` branch. commit 67f52feb97136abaeac15dc2771b8802a4a62d32 Author: Kim Morrison <[email protected]> Date: Wed Jul 31 23:15:35 2024 +0000 chore: backports for leanprover/lean4#4814 (part 6) (#15313) See https://github.com/leanprover-community/mathlib4/pull/15245 Co-authored-by: Ruben Van de Velde <[email protected]> commit 037c8b961aca6a0bd6aa45310cd2c66a14bd0aae Author: leanprover-community-mathlib4-bot <[email protected]> Date: Wed Jul 31 23:04:48 2024 +0000 chore: update Mathlib dependencies 2024-07-31 (#15372) This PR updates the Mathlib dependencies. commit e6d4b0517f82e0c97d713cd5f22a1866b9efbf0f Author: Peter Nelson <[email protected]> Date: Wed Jul 31 21:06:31 2024 +0000 feat(Order/KonigLemma): Kőnig's infinity lemma (#12273) This PR proves Kőnig's infinity lemma in terms of covers in a strongly atomic order, and it gives a common formulation for directed systems, which is useful for applications such as Ramsey theory. One of the things we needed is a `Fintype` instance for `RelEmbedding r s`. This would have caused a bad diamond with `SimpleGraph.Hom.instFintype`, so instead we remove the latter and provide their common generalization `RelHom.instFintype` in `Fintype.Pi`. commit c4b7ae4b3d3c706897e77a1489c26cbf299282fc Author: David Loeffler <[email protected]> Date: Wed Jul 31 20:15:02 2024 +0000 feat(LegendreSymbol/AddCharacter): std add char of ZMod N is primitive (#14495) The standard additive character of `ZMod N` is a primitive character. commit d487a5f28dd723638aa7d927b1e3d88c432c2e4e Author: sgouezel <[email protected]> Date: Wed Jul 31 19:18:11 2024 +0000 Chore: Remove some uses of `open Classical` (#15371) It is dangerous to `open Classical`, as it can hide that some theorem statements would be better stated with explicit decidability assumptions. This PR removes a few of them, using instead `classical` in proofs and `open Classical in ...` when needed for the statement. commit b66c970bb97db6dd93699286eb0960799bc85160 Author: Floris van Doorn <[email protected]> Date: Wed Jul 31 19:18:09 2024 +0000 feat: gcongr works with eta and proofs (#15364) * `gcongr` now recognizes eta-expanded variables as variables * `gcongr` now recognizes all proofs as "defeq" even if the proofs have different types (in e.g. `Finset.sup'_mono` * Give a bit more information in the error message when not accepting a `gcongr`-lemma. commit cdcd8836671bf0c4258e203d411790609186ddca Author: Yury G. Kudryashov <[email protected]> Date: Wed Jul 31 19:18:08 2024 +0000 chore(SimpleFunc): use `FunLike` (#6642) commit 0a717792814730b6a63765a4bb194368ee23b173 Author: Ruben Van de Velde <[email protected]> Date: Wed Jul 31 18:23:43 2024 +0000 chore: remove obsolete comments about @[congr] (#15299) Some of these have been commented out since this file was added to mathlib 3, others refer to theorems that have been upstreamed. In any case, they are not actionable. commit a3e5a2839960926e0b846c1b6c9e711fc66c03e7 Author: Dagur Asgeirsson <[email protected]> Date: Wed Jul 31 16:34:07 2024 +0000 refactor(Topology/Category): use `CompHausLike` API for limits in `LightProfinite` (#15362) commit feb80cfa4a111e7bbf7bc3af2113d035a1e7fd21 Author: Dagur Asgeirsson <[email protected]> Date: Wed Jul 31 16:34:06 2024 +0000 feat(CategoryTheory): add some instances for essentially small sites (#13486) This PR proves that the properties `PreservesSheafification` and `WEqualsLocallyBijective` hold for an essentially small site if they hold for an equivalent small site. commit ee09f89b2ba77261d634d86fa01fbab530c8e1df Author: Joachim Breitner <[email protected]> Date: Wed Jul 31 15:51:01 2024 +0000 feat(ENat): lt_add_one_iff (#15341) from the Carleson project commit 61c938b74ca184102d7c996d42553d63a2f452b0 Author: Joachim Breitner <[email protected]> Date: Wed Jul 31 14:10:54 2024 +0000 feat(ENat): sSup_mem_of_Nonempty_of_lt_top (#15347) Lemma statement due to Gareth Ma. More discussion at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/ENat.2EiSup_eq_coe_iff from the Carleson project commit 9610549d4c892f252d1bb1a96bdde7bbedb7589b Author: Frédéric Dupuis <[email protected]> Date: Wed Jul 31 13:46:32 2024 +0000 fix(ContinuousFunctionalCalculus): generalize a section from `Field R` to `Semifield R` (#15351) This PR generalizes the section that proves that `cfcₙ` is equivalent to `cfc` to `Semifield R` from `Field R`. This is crucial because this needs to work for `ℝ≥0`. commit c62c3b3606954938ff93da819945ffbf908e3df8 Author: Dagur Asgeirsson <[email protected]> Date: Wed Jul 31 13:08:31 2024 +0000 refactor(Topology/Category): preparation for switching to new API for limits in CompHaus (#15359) commit b5a3f4856644c79dd29b2c7db3ef4ec7eae9f349 Author: Kim Morrison <[email protected]> Date: Wed Jul 31 12:36:47 2024 +0000 chore: update lean4checker version (#15365) commit 5040d990226fe13a6975eee23261d1dc2b88ddaf Author: leanprover-community-mathlib4-bot <[email protected]> Date: Wed Jul 31 12:12:02 2024 +0000 chore: update Mathlib dependencies 2024-07-31 (#15354) This PR updates the Mathlib dependencies. commit a719ba5c3115d47b68bf0497a9dd1bcbb21ea663 Author: Kim Morrison <[email protected]> Date: Wed Jul 31 11:08:55 2024 +0000 chore: bump toolchain to v4.10.0 (#15361) commit 6b4579af14e39dfa82e620dbc99d2aedaabc0a55 Author: damiano <[email protected]> Date: Wed Jul 31 10:31:17 2024 +0000 fix: allow markdown in declarations_diff (#15356) This is mostly aesthetical: with the extra line break, the markdown parser kicks in, notices the backticks `` ` `` and interprets them as code. Otherwise, it prints the literal backticks. commit 012ddf4e8383aa29a077932718be59a099d4b020 Author: Ruben Van de Velde <[email protected]> Date: Wed Jul 31 09:27:50 2024 +0000 chore: improve some ext_iff lemmas (#15340) These will be auto-generated by `@[ext]` in lean v4.11; this prepares us for that change. commit 591bab05295f3406cbd106c646c6e0eea076de50 Author: Jz Pan <[email protected]> Date: Wed Jul 31 09:27:49 2024 +0000 feat(FieldTheory/IntermediateField): add `Subfield.extendScalars` (#15148) ... which can be viewed as an inverse to `IntermediateField.toSubfield`. This is similar to `IntermediateField.extendScalars`. commit 12ecba79d54f5eee2973cfdbd17dd3a4d12869d1 Author: Yury G. Kudryashov <[email protected]> Date: Wed Jul 31 09:13:22 2024 +0000 chore(LpSpace): minor golf (#15348) Reuse a proof. commit f9821a610497db923cb7eaff70f036accb1f071c Author: Emily Riehl <[email protected]> Date: Wed Jul 31 09:13:20 2024 +0000 chore: split conj into two files to streamline imports (#15300) This splits the file CategoryTheory.Conj into CategoryTheory.HomCongr and CategoryTheory.Conj. The point is that the latter requires much heavier imports than the former, while the former is all that is needed for CategoryTheory.Adjunction.Mates, which is used elsewhere. While making those changes, I added one theorem to the HomCongr file: * A theorem `map_isoCongr` which parallels the existing `map_homCongr`. The proof is by `ext; simp` once the existing `isoCongr` is tagged with simps. In parallel, I've tagged the definition `homCongr` with simps and removed the theorem `homCongr_apply` which is automatically generated by simps. commit 7f9cbc0613b2277a7c5ca8f20f965ccb8f4d4035 Author: Andrew Yang <[email protected]> Date: Wed Jul 31 09:13:19 2024 +0000 feat(AlgebraicGeometry): Define preimmersions. (#14748) commit 9c47f211ae5ce5b4778d963e30d433dfb96eb390 Author: Andrew Yang <[email protected]> Date: Wed Jul 31 08:12:19 2024 +0000 feat(RingTheory/Kaehler): Cotangent complex associated to an embedding into affine space. (#14859) Co-authored-by: Andrew Yang <[email protected]> commit 0ca50c62318a3abc46f03d2bb6848795dfa58296 Author: sgouezel <[email protected]> Date: Wed Jul 31 10:11:44 2024 +0200 start commit 1aef8600a6550e8de3bc501d66cfa5fe56f20b76 Author: Jz Pan <[email protected]> Date: Wed Jul 31 06:44:15 2024 +0000 feat: add `comap_map` for sub(semi)ring, subalgebra, subfield and intermediate fields (#15193) Generalizes `Subgroup.comap_map_eq`, `Subgroup.comap_map_eq_self`, `Subgroup.comap_map_eq_self_of_injective`, and `Subgroup.map_comap_eq`, `Subgroup.map_comap_eq_self`, `Subgroup.map_comap_eq_self_of_surjective`. commit 1409ad6a8f37874bd51e73da03b1234984b27ab9 Author: Peter Nelson <[email protected]> Date: Wed Jul 31 06:44:14 2024 +0000 feat(Data/Matroid/Sum): Sums of matroids (#15061) This PR defines the sum of a pair or collection of matroids, and gives basic API. The material in `Matroid/Map` makes this both more general and shorter than #12380 , which got a bit snarled up in review. - [x] depends on: #15060 - [x] depends on: #15057 commit 2c270faa69976f7665c1fadfebdfac9b18df0d91 Author: Dagur Tómas Ásgeirsson <[email protected]> Date: Wed Jul 31 06:44:12 2024 +0000 refactor(Topology/Category): refactor LightProfinite.Basic (#13912) This is the second part of the refactor of CompHaus and friends (refactoring the definition of `LightProfinite` in terms of `CompHausLike`, see #12930 for the end result) commit 09e1ab33b2621aba98326aee36572a878b092875 Author: Yaël Dillies <[email protected]> Date: Wed Jul 31 06:33:46 2024 +0000 chore(MeasureTheory): Rename `snorm` to `eLpNorm` (#15177) 1. `eLpNorm` for "extended Lp norm" is much more descriptive than `snorm` for "seminorm" 2. I need a `NNReal`-valued version of it, which I am planning to call `nnLpNorm`. commit 0c8f6eb2ddff2c685b309a8dd4b0f5bd9dcb30d4 Author: Aaron Anderson <[email protected]> Date: Wed Jul 31 06:03:29 2024 +0000 chore(ModelTheory/Complexity): move quantifier complexity into a new file (#15275) Several important files in the model theory library touch on quantifier complexity of formulas, an idea that is not yet used for anything else in `mathlib`. This PR moves all quantifier complexity content to a new file, `ModelTheory/Complexity` and improves the documentation of these concepts. This will hopefully make these basic files more legible and easier to refactor. Co-authored-by: Aaron Anderson <[email protected]> commit 4235d67fc874159299b7ff8759ac3af1ad750f42 Author: Yaël Dillies <[email protected]> Date: Wed Jul 31 05:14:53 2024 +0000 feat: Lemmas specialised to `piFinset fun _ : Fin n ↦ s` (#15329) Those lemmas are specifically useful for rewriting backwards when the indexing type doesn't matter (and also sometimes useful forwardly). From LeanAPAP commit c934de62defa99cdb760c5b9165d67c459805253 Author: Kim Morrison <[email protected]> Date: Wed Jul 31 03:44:36 2024 +0000 chore: backports for leanprover/lean4#4814 (part 9) (#15352) see https://github.com/leanprover-community/mathlib4/pull/15245 commit 7c70ad9dd4cfd5a737e98022fa32092c5764508e Author: Ruben Van de Velde <[email protected]> Date: Wed Jul 31 02:43:56 2024 +0000 chore: move Init.Order.Defs to Order.Defs (#15210) commit 59d4157413e8bb064ee7071eb787bd91a7662587 Author: Matthew Robert Ballard <[email protected]> Date: Wed Jul 31 01:56:00 2024 +0000 chore (Algebra.Order.Ring.Unbundled.Basic): inline typeclass assumptions (#15334) We improve the generality of the results here by using inlined typeclass assumptions. It also makes this file comport better with the new variable inclusion mechanism. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/New.20variable.20inclusion.20mechanism). Co-authored-by: Kim Morrison <[email protected]> commit 876ccfb5f92cb397a40b4c53ff9c09dcdf23debd Author: blizzard_inc <[email protected]> Date: Wed Jul 31 01:05:54 2024 +0000 chore: backports for leanprover/lean4#4814 (part 7) (#15332) see https://github.com/leanprover-community/mathlib4/pull/15245 Co-authored-by: Kim Morrison <[email protected]> commit ce4bc7a4eded7cd1f6f6d8b2cae541d3fdb7eb5f Author: grunweg <[email protected]> Date: Tue Jul 30 19:21:45 2024 +0000 chore: fix Lean 3 names in comments, related to presheaves (#15308) Rename - presheaf -> Presheaf - opens -> Opens - supr -> iSup - pairwise -> pairwise - and a few more commit ad356e50eff01c901685b1c5ee8afd3bfed7f9c3 Author: Yury G. Kudryashov <[email protected]> Date: Tue Jul 30 18:20:59 2024 +0000 chore(Topology/LocallyClosed): move around (#15323) - move definitions to `Topology/Defs/Basic`; - move the last lemma to `Topology/LocalAtTarget`. commit b0a0fca7e605f534899cc7b7f69af2d830825c94 Author: Yuma Mizuno <[email protected]> Date: Tue Jul 30 17:49:45 2024 +0000 feat: string diagram widget (#10581) Add the widget to display string diagram of monoidal category morphism. commit 21128b8403fadf423d252694092820036ff39174 Author: Yaël Dillies <[email protected]> Date: Tue Jul 30 17:21:12 2024 +0000 chore: Generalise `Pi.exists_forall_pos_add_lt` to monoids (#15327) ... as spotted by Yury. commit 31fb8cf3bbe4c5cd1517e1e16c9d60d1743dd183 Author: grunweg <[email protected]> Date: Tue Jul 30 17:21:11 2024 +0000 chore: rename is_limit -> isLimit in a local variable (#15309) It refers to a `IsLimit` hypothesis: probably, this name is still a leftover from mathlib3. commit db8dc843e42d4ce957d1919227451a23c24d7b95 Author: Yaël Dillies <[email protected]> Date: Tue Jul 30 16:56:27 2024 +0000 feat: Monotonicity of multiplication by positive rationals (#15328) From LeanAPAP commit 99914c5468aa35e6cc8fe115b2ce8c145fe3c11d Author: Yury G. Kudryashov <[email protected]> Date: Tue Jul 30 16:56:25 2024 +0000 chore(LocallyConvex/Bounded): rename `variable`s (#15289) Instead of introducing a normed field `𝕜` and a nontrivially normed field `𝕝`, prove a theorem for a normed field, then assume that `𝕜` is a nontrivially normed field. commit 245de8ade497db1962bdcbbb7242dace0f77adb1 Author: Yury G. Kudryashov <[email protected]> Date: Tue Jul 30 16:56:24 2024 +0000 chore(NormedSpace/Multilinear): drop `DecidableEq` assumptions (#15268) commit c26d054d87de0515863eb215e2d6602e6d5acd7f Author: Yaël Dillies <[email protected]> Date: Tue Jul 30 16:32:12 2024 +0000 chore(Corner/Defs): Fix copy-pasta (#15325) Some brain (mine) was non functioning at the time of writing. commit a9b958379044c5e9d11c4c97fce99dd58036b406 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Tue Jul 30 16:32:10 2024 +0000 chore: update Mathlib dependencies 2024-07-30 (#15317) This PR updates the Mathlib dependencies. commit e7b14b1e122554fef8e607d89be99c0215a51fa1 Author: Dagur Tómas Ásgeirsson <[email protected]> Date: Tue Jul 30 16:32:09 2024 +0000 refactor(Topology/Category): refactor Stonean.Basic (#13911) This is the second part of the refactor of CompHaus and friends (refactoring the definition of `Stonean` in terms of `CompHausLike`, see #12930 for the end result) commit 53c5e956497733a070038665bb1706d685fc874a Author: Joël Riou <[email protected]> Date: Tue Jul 30 16:14:35 2024 +0000 feat(CategoryTheory): preservation of pullback/pushout squares (#15044) The main result in this PR is that a commutative square `sq : Square C` is a pullback square iff it is mapped to a pullback square in the category of types when we apply the functor `coyoneda.obj X` for any `X : Cᵒᵖ`. In order to do this, it is shown that the proprety `Square.IsPullback` is preserved when a functor preserving this pullback is applied. A similar result is obtained for pushout squares, which required developing the "opposites" API for squares. commit 9b81e4dd8d0ccb00f33b18e8b905c333e7068a87 Author: Yury G. Kudryashov <[email protected]> Date: Tue Jul 30 15:11:48 2024 +0000 docs(MkIffOfInductiveProp): fix typos (#15324) commit 3cf5b30cbc3e38c11076c6c632cbd562c1bb51a4 Author: Yury G. Kudryashov <[email protected]> Date: Tue Jul 30 15:11:47 2024 +0000 chore(VitaliFamily): fix `open`/`open scoped` (#15320) commit a38e18732a67e94cf7e62d3c6cf399500ff7a6d9 Author: damiano <[email protected]> Date: Tue Jul 30 15:11:46 2024 +0000 chore: style adjustments (#15319) commit 0bc17f8830b66da55cc322e18872498301cb550e Author: grunweg <[email protected]> Date: Tue Jul 30 15:11:45 2024 +0000 chore(TensorProduct/RightExactness): move three lemmas to Algebra/Exact (#15032) The location was suggested by #find_home. This addresses a porting TODO. commit df2eea5e25e8b5d262cd5ce237c6dd9335a98d22 Author: Kim Morrison <[email protected]> Date: Tue Jul 30 13:32:35 2024 +0000 chore: backports for leanprover/lean4#4814 (part 5) (#15310) See https://github.com/leanprover-community/mathlib4/pull/15245 commit 48bbda473582651a16781cac069b4754d990b9aa Author: Andrew Yang <[email protected]> Date: Tue Jul 30 13:16:25 2024 +0000 feat(Algebra/Category/Ring): Add dsimp lemmas for `CommRingCat`. (#15297) Co-authored-by: Andrew Yang <[email protected]> commit 254c0af36609421f795d162f7269c2b0ecb0c44f Author: grunweg <[email protected]> Date: Tue Jul 30 12:37:45 2024 +0000 chore(HahnBanach/SeparatingDual): Finite -> Fintype (#15305) Found by the linter in #10235. commit 2a73834eb36aae4e1107237dcc9cee1c0c0eb5d7 Author: grunweg <[email protected]> Date: Tue Jul 30 12:27:53 2024 +0000 chore(Combinatorics): remove superfluous use of DecidableEq (#15306) Found by the linter in #10235. commit 812748cd2eecd0f3f852a8a76ccefb3cd28c7527 Author: Johan Commelin <[email protected]> Date: Tue Jul 30 12:11:37 2024 +0000 chore(scripts/create-adaptation-pr): abort whenever command fails (#15298) commit 0f83d8791efd6c93eac8bddf0b7d534813824eaf Author: María Inés de Frutos-Fernández <[email protected]> Date: Tue Jul 30 11:18:19 2024 +0000 feat(Analysis.Normed.Ring.SeminormFromConst): add seminormFromConst (#14361) We prove [BGR, Proposition 1.3.2/2] : starting from a power-multiplicative seminorm on a commutative ring `R` and a nonzero `c : R`, we create a new power-multiplicative seminorm for which `c` is multiplicative. commit be0314103abe699d41b5220e41210ef0e8dd95f5 Author: Rémy Degenne <[email protected]> Date: Tue Jul 30 09:34:55 2024 +0000 feat: add `Pairwise.pairwiseDisjoint` (#15292) `Pairwise (Disjoint on f)` implies `s.PairwiseDisjoint f` for any set `s`. Co-authored-by: Rémy Degenne <[email protected]> commit 71d4424ecc0ebadb2f8a274514623dbbe5754efb Author: Johan Commelin <[email protected]> Date: Tue Jul 30 08:44:27 2024 +0000 chore(GroupTheory/GroupAction/Quotient): fix to_additive names (#15293) commit c1478df31c247d1fd6538b64eea4ea388be7ed96 Author: Yury G. Kudryashov <[email protected]> Date: Tue Jul 30 08:44:26 2024 +0000 chore(DirectSum): drop `DecidableEq` assumption (#15287) Co-authored-by: Michael Rothgang <[email protected]> commit 7cd5c43f144c68dc0dd47afe2b033c33936af7eb Author: Yury G. Kudryashov <[email protected]> Date: Tue Jul 30 08:33:33 2024 +0000 chore(NumberTheory): drop some `DecidableEq` assumptions (#15288) commit 74f1093c6c00c4a5c0db306bfbddd3526f68703e Author: Pim Otte <[email protected]> Date: Tue Jul 30 08:33:31 2024 +0000 feat(Combinatorics/SimpleGraph/Connectivity): getVert lemmas (#14977) Add some lemmas about `SimpleGraph.Walk.getVert`. In preparation for Tutte's theorem. commit 8e3c880153d8878c28fcc2793644f35f9c7434a6 Author: Yury G. Kudryashov <[email protected]> Date: Tue Jul 30 08:12:24 2024 +0000 feat(MeasurePreserving): use `NullMeasurableSet` (#15098) commit 38c577df552816a8e098e9b37e1fd6969bceb3bd Author: Christopher Hoskin <[email protected]> Date: Tue Jul 30 05:32:07 2024 +0000 feat(algebra/hom/centroid): Centre of the Centroid of a *-ring is a *-ring (#6595) This PR shows that the centre of the centroid of a *-ring is a *-ring. Previously submitted to mathlib as https://github.com/leanprover-community/mathlib/pull/18096 Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> commit 2609c03c1ca0e6245da471339e408aa370bb7c36 Author: Rida Hamadani <[email protected]> Date: Tue Jul 30 05:14:52 2024 +0000 refactor(Combinatorics/SimpleGraph): move `Walk` to its own file (#15171) split `Path` and higher into a separate file from `Walk` Co-authored-by: Parcly Taxel <[email protected]> commit 43adf291bd857560331caf525ae53d50f400206f Author: leanprover-community-mathlib4-bot <[email protected]> Date: Tue Jul 30 03:18:28 2024 +0000 chore: update Mathlib dependencies 2024-07-30 (#15281) This PR updates the Mathlib dependencies. commit 31b40b49fb1449551e895cfeb1c369aad65bd32c Author: Scott Carnahan <[email protected]> Date: Tue Jul 30 02:04:06 2024 +0000 feat (LinearAlgebra/RootSystem/RootPositive) : Root-positive bilinear forms (#15155) This PR introduces a Prop-valued mixin class for root pairings, specifying that a bilinear form on weight space is symmetric, reflection-invariant, and gives roots a strictly positive norm. Given a root-positive norm, one obtains sign-compatibilities between the form and the canonical pairing between roots and coroots. Root-positive forms show up naturally in Kac-Moody Lie algebras (without the name), and the canonical polarization on a finite root pairing induces a root-positive form. commit ee1fbad99e52a033b93cf2c6579a912cce569a4d Author: Kim Morrison <[email protected]> Date: Tue Jul 30 01:09:55 2024 +0000 chore: backports for leanprover/lean4#4814 (part 4) (#15255) See https://github.com/leanprover-community/mathlib4/pull/15245 commit 9f4987a1cf1ffe1323d717b9fdedb9c8691dbffb Author: grunweg <[email protected]> Date: Tue Jul 30 00:15:49 2024 +0000 chore(Algebra): remove superfluous DecidableEq hypotheses (#15278) Found by the linter in #10235. commit d78ec33d35d7a47beec441a5c6f7ded6bd25742a Author: Kim Morrison <[email protected]> Date: Tue Jul 30 00:15:48 2024 +0000 chore: replace zip_with -> zipWith in lemma names (#15218) commit 190a3318ffe9c5c22c7d7b9eeb643dc409cc7505 Author: grunweg <[email protected]> Date: Tue Jul 30 00:05:14 2024 +0000 chore(Combinatorics/HalesJewett): replace Fintype -> Finite (#15279) Found by the linter in #10235. commit ba4821dfe3d90f9c4992fd88b2dd394dc5fbaed8 Author: Patrick Massot <[email protected]> Date: Mon Jul 29 21:21:20 2024 +0000 lRevert "Add a bot posting event reminders on Zulip" (#15272) This was pushed to master by accident This reverts commit 924277adf1e97d31a15cb23a9bfc9a78062d6b48. commit d56fbc322424d6646e945f431750a23be9f47768 Author: Rida Hamadani <[email protected]> Date: Mon Jul 29 21:02:54 2024 +0000 refactor(Combinatorics/SimpleGraph): rename `Connectivity.lean` to `Walk.lean` (#15273) commit f5703e8116fb49eee6a6cdf3259c604c62f5c081 Author: Andrew Yang <[email protected]> Date: Mon Jul 29 20:50:13 2024 +0000 chore(AlgebraicGeometry): Rename `openCoverOfSuprEqTop` to `openCoverOfISupEqTop` (#15079) commit 17008649d994c4238fa1b6a709c37290e5acc2b8 Author: grunweg <[email protected]> Date: Mon Jul 29 19:04:19 2024 +0000 style: remove more trailing semicolons (#15011) commit a01f1cc5e9957296c1d51063367bfdf3e4afed21 Author: Christian Merten <[email protected]> Date: Mon Jul 29 18:29:50 2024 +0000 refactor(AlgebraicGeometry): stalk maps (#15070) Introduces `Scheme.Hom.stalkMap` and `LocallyRingedSpace.Hom.stalkMap` with the API copied from presheafed spaces. Removes `LocallyRingedSpace.stalk` and `LocallyRingedSpace.ΓToStalk`. Instead uses `Presheaf.stalk` and `Presheaf.germ` directly. Co-authored-by: Andrew Yang <[email protected]> Co-authored-by: Andrew Yang <[email protected]> Co-authored-by: erdOne <[email protected]> commit bb85073b9fa01e154556d21eec50f489f730b253 Author: Rida Hamadani <[email protected]> Date: Mon Jul 29 17:43:43 2024 +0000 docs(Topology): add tag to one-point compactification (#15266) commit 4196dc8af7e7140f2d3f4384e2e1785808b00c1d Author: Chris Birkbeck <[email protected]> Date: Mon Jul 29 17:43:42 2024 +0000 feat: define logarithmic derivatives (#12804) We define the logarithmic derivative of a function as `f'/f` and then prove some basic facts about this. Specifially some things that will be needed for the Mittag-Leffler Expansion for Cotangent Function. Co-authored-by: Chris Birkbeck <[email protected]> Co-authored-by: Yury G. Kudryashov <[email protected]> commit 36b887b1e148032d368fc09fd64565362393ea7f Author: Yury G. Kudryashov <[email protected]> Date: Mon Jul 29 17:16:33 2024 +0000 feat(LiminfLimsup): drop unneeded `DecidableEq` assumptions (#15267) commit fdd94c07a3e6d252e84f12e394085868d7794d68 Author: Joachim Breitner <[email protected]> Date: Mon Jul 29 16:50:02 2024 +0000 feat(Order/Minimal): generalize PartialOrder to Preorder where possible (#15196) from the Carleson project. commit 924277adf1e97d31a15cb23a9bfc9a78062d6b48 Author: Patrick Massot <[email protected]> Date: Mon Jul 29 18:43:11 2024 +0200 Add a bot posting event reminders on Zulip commit 54129d0f67ddb81b3da642352febc0eb628ef6f0 Author: Kevin Buzzard <[email protected]> Date: Mon Jul 29 13:52:10 2024 +0000 feat(Mathlib/NumberTheory/FLT/Basic): expand module docstring. (#15263) Add historical references and reference to ongoing formalisation of FLT. commit a1db8c708c4f93a263948086cdf23769913a31b9 Author: Kim Morrison <[email protected]> Date: Mon Jul 29 07:19:44 2024 +0000 chore: backports for leanprover/lean4#4814 (part 3) (#15249) See https://github.com/leanprover-community/mathlib4/pull/15245 commit 1d0802459cf6723917d3804cbd92f87c08847a46 Author: Etienne <[email protected]> Date: Mon Jul 29 07:19:43 2024 +0000 feat: Rename `CompactlyGeneratedSpace` to `UCompactlyGeneratedSpace` (#15201) `CompactlyGeneratedSpace` is defined in `Mathlib.Topology.Category.CompactlyGenerated`. Due to functors considerations, the definition involves a free universe parameter, which is not desirable for topological purposes. Therefore we rename `CompactlyGeneratedSpace` to `UCompactlyGeneratedSpace` so that `CompactlyGeneratedSpace` can be defined as a special case. This was discussed [here](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Compactly.20generated.20spaces/near/453957506). commit bc33405d6e3f9c36e0167b627229a2072d41661c Author: Peter Nelson <[email protected]> Date: Mon Jul 29 07:19:42 2024 +0000 feat(Data/Matroid/Map): add missing lemmas (#15060) We add a few missing lemmas, mostly about `Matroid.Basis`, in `Matroid/Map`, and also fix a couple of typos in the same file. commit 29fe1f7e9a4ab395bb7cf1d78d5d2d823e51cc9a Author: Yaël Dillies <[email protected]> Date: Mon Jul 29 07:19:40 2024 +0000 feat: The multinomial theorem in terms of `piAntidiag` (#14998) Prove that `(∑ i in s, f i) ^ n = ∑ k in piAntidiag s n, multinomial s k * ∏ i in s, f i ^ k i`. We already have a version of this for `Finset.sym`, so I am also adding machinery to deduce one from the other. I however haven't managed to do that. From LeanAPAP commit 91e63eb92add229f01451997a8bb58078c740210 Author: grunweg <[email protected]> Date: Mon Jul 29 06:28:27 2024 +0000 chore: more fixes for the flexible linter (#15130) commit c0604e0c3c134649bc4e8988ab0619e22d67f344 Author: damiano <[email protected]> Date: Mon Jul 29 05:46:40 2024 +0000 chore: replace forall intro in UnsignedHahn (#15205) This file (and specifically [MeasureTheory.hahn_decomposition](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Decomposition/UnsignedHahn.html#MeasureTheory.hahn_decomposition), the only declaration that it contains) stumps a linter that looks for "collapsible" pairs `forall`/`intro`. `have d_split` used to have a `MeasurableSet s` assumption, but it was unnecessary and I removed it. Strictly speaking, this was not needed for my purpose, but I noticed it thanks to the linter. commit 188a24253ae09e6b6326655e77a9729098a410fd Author: damiano <[email protected]> Date: Mon Jul 29 04:45:57 2024 +0000 CI: install elan in `lint_and_suggest`, suggest import changes (#15250) The `lint` step in [this action](https://github.com/leanprover-community/mathlib4/actions/runs/10137312257/job/28027367787?pr=15250) used to fail. Also added reviewdog suggestion to propose adding missing `import`s in "import all" files. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/silent.20CI.20lint.20error/near/454527007) commit 2159435a6c8f23ffbb051a3667af1134924a4192 Author: Geoffrey Irving <[email protected]> Date: Mon Jul 29 03:09:52 2024 +0000 feat: Define `AnalyticWithinAt` and `AnalyticWithinOn` (#13971) Unlike `ContinuousOn`, which allows arbitrary behavior outside of the set, `AnalyticOn` requires the function to be analytic in a neighborhood of the set. This is inconvenient for analytic manifolds with boundary, as we want analyticity for functions meaningful only up to the boundary. Here we add `AnalyticWithinAt` and `AnalyticWithinOn` with the natural definitions. The one subtlety is that we explicitly require `ContinuousWithinAt` in `AnalyticWithinAt`, as otherwise the natural definition does not imply a nice value of the function at the point. Co-authored-by: Yury G. Kudryashov <[email protected]> commit e670f86796659643582c68df07b6a1c286280824 Author: damiano <[email protected]> Date: Mon Jul 29 01:34:14 2024 +0000 fix: re-add the `TextBased` long line linter (#15190) As pointed out on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Long.20lines.20linter.20regression), the `TextBased` long line linter should not have been removed. There are two advantages to having also the `TextBased` linter: * if you accidentally submit code with long lines, the `TextBased` linter will tell you of all long lines at once; * the linter can only flag lines on files that import the linter, while the `TextBased` linter crawls all `.lean` files in `Mathlib`. commit 04e23488cdc6c40e3480f98100698e0566c1c192 Author: blizzard_inc <[email protected]> Date: Sun Jul 28 23:33:41 2024 +0000 chore: robustifying for debug.byAsSorry (part 13) (#15197) commit e026b770249e6b8298d7d8b8360030d084659770 Author: Aaron Anderson <[email protected]> Date: Sun Jul 28 23:22:41 2024 +0000 chore(ModelTheory/Encoding): improve the encoding of formulas to avoid `sizeOf` (#15209) Edits the decoding of lists into first-order formulas, so that the proof of well-foundedness is easier and no longer invokes `sizeOf`. commit 9ca8f83e2b3aa96eb56517130b850f7adaef51b2 Author: damiano <[email protected]> Date: Sun Jul 28 21:26:37 2024 +0000 fix: the long line linter only acts on mathlib (#15226) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315097.20the.20long.20line.20linter.20as.20a.20syntax.20linter/near/453908911) commit 663a7b8edd3718b4a8d05c8c1e5a6d504116d0db Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 21:09:13 2024 +0000 chore(InnerProductSpace/PiL2): `Fintype m` -> `Finite m` (#15232) commit be90435eb8a9294961668ca316fdbcf4d8396b51 Author: damiano <[email protected]> Date: Sun Jul 28 20:59:26 2024 +0000 docs: add module docs for `declarations_diff` (#15195) This PR adds documentation to the `declarations_diff` script. Consequence of #15149. commit 80fec67dbc0563d13951c5ad49c2e97b36345311 Author: Bjørn Kjos-Hanssen <[email protected]> Date: Sun Jul 28 20:36:28 2024 +0000 doc: add a warning that `comap` is zero for non-injective functions (#15220) commit 03943935c141b0433a3decceab05c2e4076201bc Author: vin-gui <[email protected]> Date: Sun Jul 28 19:58:52 2024 +0000 feat: proper group actions (#11746) We define proper action of a group on a topological space, and we prove that in this case the quotient space is T2. We prove that if a Hausdorff group acts properly on $X$, then $X$ is Hausdorff. We also give equivalent definitions of proper action using ultrafilters and show the transfer of proper action to a closed subgroup. We show that if $X \times X$ is Hausdorff and compactly generated then the action is properly discontinuous if and only if it is continuous in the second variable and proper in the sense defined here. The "compactly generated" assumption is to be rephrased with typeclass inference in the future. Co-authored-by: @EtienneC30 Co-authored-by: @florestan Co-authored-by: @ADedecker Co-authored-by: Etienne <[email protected]> Co-authored-by: ADedecker <[email protected]> Co-authored-by: florestan <[email protected]> commit 65c21dc162fe04abdd252ebb993025309cb60cb6 Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 19:09:17 2024 +0000 chore(RingTheory): fix `DecidableEq` and `Fintype` vs `Finite` (#15236) commit 45c24fbe8c4c21118c5101f74963077cdb555525 Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 19:09:15 2024 +0000 chore(Matrix/RowCol): `Inhabited` -> `Nonempty` (#15235) commit 05d6576e142878b8cf97ebd880781d9f9a0da93d Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 19:09:14 2024 +0000 chore(SobolevInequality): drop a `DecidableEq` assumption (#15230) commit 145c77aa451fe71e59479810c9ee7c5239167e3f Author: María Inés de Frutos-Fernández <[email protected]> Date: Sun Jul 28 19:09:13 2024 +0000 feat(Topology/Algebra/Algebra): add ContinuousAlgHom (#12800) We add the type `ContinuousAlgHom` for continuous algebra homomorphisms. Co-authored-by: Antoine Chambert-Loir <[email protected]> Co-authored-by: Antoine Chambert-Loir <[email protected]> commit 812fe7140fe8b68c9023f58b9ed2be7d959528de Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 18:21:53 2024 +0000 chore(Combinatorics): drop some `DecidableEq` assumptions (#15233) commit f839c3ec131876a32189c8f01553910b5c636374 Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 18:21:52 2024 +0000 chore(Topology/Algebra/UniformConvergence): golf (#15216) commit 480bf95a5f58a16ee1e0dff235315581eb7173da Author: Yaël Dillies <[email protected]> Date: Sun Jul 28 18:21:51 2024 +0000 chore: Move `DistribMulAction` on `Opposite`, `Pi`, `Prod`, `Sum`, `Sigma`, `Units` (#14937) commit 70c21a9665423338cb2fe242c4a797663557935e Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 18:21:50 2024 +0000 feat(GroupAction/IterateAct): new file (#14891) commit 5211b31040dc516c6ab2f73c2fbf7dd02b89cd89 Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 18:01:02 2024 +0000 chore(Convex/Combination): use `Finite`, not `Fintype` (#15227) commit c9b4c449e1ebe5db4466dc8d46b681eec6d75afb Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 18:01:01 2024 +0000 chore(NumberField/Discriminant): golf (#15223) Use `calc` to golf a proof and improve readability. commit ca528de4aeac718edaced38494759ef704a26f43 Author: Yury G. Kudryashov <[email protected]> Date: Sun Jul 28 17:51:03 2024 +0000 chore(Convex/Radon): drop `DecidableEq` assumptions (#15234) commit ff20ec3a42e6edf3561619a429fdb3a2812ffe5f Author: grunweg <[email protected]> Date: Sun Jul 28 17:32:33 2024 +0000 chore: normalise authors line in copyright header (#15231) Two test files used 'Author', but had multiple authors. This is both absurd and violates the style guide. commit caac5b13fb72ba0c5d0b35a0067de108db65e964 Author: Kevin Buzzard <[email protected]> Date: Sun Jul 28 16:59:53 2024 +0000 feat: topology on ring of finite adeles. (#14176) Use `SubmodulesRingBasis` to put a topology on the finite adeles. commit 07ede5049b7a9e02db2803d6c0f549d983f95fee Author: Yaël Dillies <[email protected]> Date: Sun Jul 28 16:06:19 2024 +0000 feat: The Erdős–Ginzburg–Ziv theorem (#14000) Prove the Erdős–Ginzburg–Ziv theorem as a corollary of Chevalley-Warning. This theorem states that among any (not necessarily distinct) `2 * n - 1` elements of `ZMod n`, we can find `n` elements of sum zero. commit 578cdceb1135e9a22bc9f61e700668bdc8076e95 Author: Calle Sönne <[email protected]> Date: Sun Jul 28 12:04:51 2024 +0000 feat(Bicategory/Functor): add more API for functors of bicategories (#15194) This PR adds some API for using different versions/rearrangements of the defining properties of lax/oplax/pseudo-functors commit 65b8389eb3b287fdf2de9ad8a8170bac00d8b710 Author: Yaël Dillies <[email protected]> Date: Sun Jul 28 10:33:19 2024 +0000 chore(MeasureTheory/Constructions/Polish): split off embedding into the reals (#15208) Credit Rémy for https://github.com/leanprover-community/mathlib3/pull/18881 commit 5644f0df4863e1d8810bbfc0652fe64376711992 Author: Etienne <[email protected]> Date: Sun Jul 28 10:01:07 2024 +0000 style: Wrong capital letter (#15211) It should be `compactSpace` rather than `compactSPace`. commit 85db8c7fd2bcb8d447952bf124670d70e3815d10 Author: Jireh Loreaux <[email protected]> Date: Sat Jul 27 23:23:26 2024 +0000 feat: generalize `Int.cast_nonneg` and related lemmas (#15186) commit 45689f00c1e0e0c7a971d504326205a5bcc36f6b Author: grunweg <[email protected]> Date: Sat Jul 27 23:01:29 2024 +0000 chore: remove some obsolete porting notes mentioning noncomputable (#15172) - Two porting notes are obsolete: the `noncomputable` modifier could simply be removed. - A few others don't seem actionable. - lean4#2077 is fixed now: no point referencing this issue any more (The `noncomputable` needs to stay, as the definition relies on other noncomputable items.) commit ed41c0c592f8953eb834ec1bf03c137ab4d5cee7 Author: Yaël Dillies <[email protected]> Date: Sat Jul 27 19:36:13 2024 +0000 feat: `OfNat.ofNat n • x = n • x` and `Nat.cast n • x = n • x` (#14997) commit cfbc1bd29c39a1920128b78fbda73fe03c58c856 Author: Yaël Dillies <[email protected]> Date: Sat Jul 27 18:20:50 2024 +0000 chore(Polynomial/UnitTrinomial): Don't import the fundamental theorem of algebra (#15207) Split the one lemma that requires it to a new file `Analysis.Complex.Polynomial.UnitTrinomial`. Also move `Analysis.Complex.Polynomial` to `Analysis.Complex.Polynomial.Basic`. commit 6d2289f1eb89535f2d22dfff6fad9b57580f82cb Author: Etienne <[email protected]> Date: Sat Jul 27 18:20:49 2024 +0000 feat: The subtype coercion associated to a closed subset is a closed map (#15202) Prove that the subtype coercion associated to a closed subset is a closed map. commit 2f4b72e2c8edde896acfbe4c49215206e28c54a8 Author: Etienne <[email protected]> Date: Sat Jul 27 17:49:22 2024 +0000 feat: ULift of a compact space is compact. (#15176) `ULift` of a compact space is compact. commit 286821d41b47c7f12879a550273e1a0a1dcd864d Author: Ruben Van de Velde <[email protected]> Date: Sat Jul 27 16:57:24 2024 +0000 chore: qualify uses of ext and ext_iff lemmas (#15106) These will become protected in lean v4.11; it is easier to land these preparations in advance. commit 946985dad875e44d65cff9f83eef5e6d6fe8148e Author: Frédéric Dupuis <[email protected]> Date: Sat Jul 27 16:22:57 2024 +0000 feat: add `NormedSpace.Core` structure to easily define normed vector spaces (#13424) This PR introduces a `NormedSpace.Core` structure loosely based on `InnerProductSpace.Core`, which encapsulates the minimal axioms needed to show that a type forms a normed vector space, as found in textbooks. We then provide functions that take a `NormedSpace.Core` and produce instances of `NormedAddCommGroup` and `NormedSpace`. Note that as it stands, defining a normed vector space from scratch (i.e. on a type without a preexisting notion of distance) is surprisingly painful, we have to keep converting between norm and distance, and there are many redundant proofs to provide. Update (2024-07-25): This PR has now been significantly expanded to include tools to add a norm structure to a type that already has a uniformity or bornology. This involves "replacing" the uniformity/bornology induced by the norm by the preexisting one, while ensuring that the uniformity/bornology induced by the norm is a equal to the old one. (This is fairly common for e.g. matrices, where all reasonable norms induce the product uniformity.) commit 933a497689bd52c74196a03de5cbf85650854d9e Author: Rida Hamadani <[email protected]> Date: Sat Jul 27 14:22:59 2024 +0000 feat(Combinatorics/SimpleGraph): define `edist` and rewrite `dist` (#14582) Define `edist` as the extended distance between two vertices of a simple graph, belonging to `ENat`, and rewrite `dist` as the coercion of `edist` to `Nat` using `toNat`. Rewrite the API to meet these new definitions. Co-authored-by: Bhavik Mehta <[email protected]> Co-authored-by: Rida Hamadani <[email protected]> commit 8fab0cc6883b147f6819d73d7b805aa49b16cf81 Author: Jireh Loreaux <[email protected]> Date: Sat Jul 27 10:36:33 2024 +0000 feat: `ZeroLEOneClass` for `StarOrderedRing` (#15185) commit 743021e758dcd82dc30fd4e97ee799645331b825 Author: blizzard_inc <[email protected]> Date: Sat Jul 27 08:25:58 2024 +0000 chore: robustifying for debug.byAsSorry (part 12) (#15178) commit 6534c8596d8efcc1a5b104f6ff5facf222d8acb4 Author: blizzard_inc <[email protected]> Date: Sat Jul 27 08:25:57 2024 +0000 chore: robustifying for debug.byAsSorry (part 11) (#15169) commit e4a1af96251737ba225014df63090041c924978a Author: blizzard_inc <[email protected]> Date: Sat Jul 27 08:25:55 2024 +0000 chore: robustifying for debug.byAsSorry (part 10) (#15164) commit 319e0a1a4391701b03063d92f3e2010644f83bd0 Author: Kim Morrison <[email protected]> Date: Sat Jul 27 07:35:01 2024 +0000 chore: robustifying for debug.byAsSorry (part 8) (#15149) See [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Running.20Mathlib.20under.20.60set_option.20debug.2EbyAsSorry.60). commit 3e862f1fb31e9a4cee3d9c57c8306449622962ca Author: Jireh Loreaux <[email protected]> Date: Sat Jul 27 07:13:08 2024 +0000 chore: move files into new `Analysis.Normed.Operator` (#15182) commit 80ee856708b04d7bd87acbd18de771592e3d9331 Author: Jireh Loreaux <[email protected]> Date: Sat Jul 27 06:01:37 2024 +0000 chore: move files into new `Analysis.Normed.Module` (#15183) commit 07aa534f61465eaf24702863984296e51399286c Author: Daniel Weber <[email protected]> Date: Sat Jul 27 05:46:45 2024 +0000 feat: define the derived set (#14834) Define the derived set of a set, and prove some properties. Also prove `AccPt.map`. Co-authored-by: Daniel Weber <[email protected]> commit 926984ff069daefc3c08c52893895a63f7c4b31b Author: damiano <[email protected]> Date: Sat Jul 27 00:45:34 2024 +0000 fix: add check for existing filepath (#15179) This should fix a problem with the online lean server [Reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/reading.20the.20.22visible.22.20file.2C.20rather.20than.20the.20saved.20one/near/454337536) commit 30361bf19c728ee033db6e5d9675c8f16e5c03f8 Author: Eric Wieser <[email protected]> Date: Fri Jul 26 21:05:01 2024 +0000 feat: add `SMul` instances to `Basis` (#14945) [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Renaming.20.60Basis.2Esmul.60/near/452825113) for the naming clash. commit beae9f43301fe2d445e7721f328ba392318fe995 Author: grunweg <[email protected]> Date: Fri Jul 26 20:04:50 2024 +0000 doc(Topology/PartitionOfUnity): add missing documentation (#15175) commit 77616f4991556951a9ab5df6fc0acbe9b7dd19c5 Author: Etienne <[email protected]> Date: Fri Jul 26 19:54:50 2024 +0000 feat: Convergence of coe to `OnePoint` (#15174) The coercion from `X` to `OnePoint X` tends to infinity along `coclosedCompact`. commit 466a8e2eaf9ded8dc6ec4da2db91987d8ac8a5c6 Author: grunweg <[email protected]> Date: Fri Jul 26 19:28:15 2024 +0000 chore(BohrMollerup): move convexity lemmas to Analysis.Convex.Function (#15031) Addresses a porting TODO commit fd199c57de42c9eea080074a4561cf0a4bcfff8d Author: Jireh Loreaux <[email protected]> Date: Fri Jul 26 17:44:33 2024 +0000 chore: create `Analysis.CstarAlgebra` folder (#15165) commit ec5a0166a29a02ba9c8407c4bb87300771b1408f Author: leanprover-community-mathlib4-bot <[email protected]> Date: Fri Jul 26 17:27:24 2024 +0000 chore: update Mathlib dependencies 2024-07-26 (#15153) This PR updates the Mathlib dependencies. commit f1c4f66688b6973de63209b9641a1ca725c77f58 Author: Jireh Loreaux <[email protected]> Date: Fri Jul 26 16:58:01 2024 +0000 chore: move files into `Analysis.Normed.Lp` (#15166) commit 6841e1d63c15394338b876e95dcda33b08f9e70f Author: Joël Riou <[email protected]> Date: Fri Jul 26 16:47:28 2024 +0000 feat(CategoryTheory/Sites): definition of Mayer-Vietoris squares (#14959) This PR introduces the very basic definitions of Mayer-Vietoris squares. It shall be expanded in future PRs towards the construction of Mayer-Vietoris long exact sequences in sheaf cohomology. Co-authored-by: Joël Riou <[email protected]> commit 5f8040b138d7b688956983d171461041f1591f73 Author: Jireh Loreaux <[email protected]> Date: Fri Jul 26 16:19:06 2024 +0000 chore: move `NormedSpace.Units` into `Normed.Ring` (#15163) commit 885c8b79410325352725d3865894e597b67a9596 Author: Pietro Monticone <[email protected]> Date: Fri Jul 26 14:49:49 2024 +0000 chore(Algebra/Module/Equiv): clean and golf (#15151) commit 624027c70e50176836da5df12ad48c42a7146c6a Author: grunweg <[email protected]> Date: Fri Jul 26 14:39:07 2024 +0000 chore: remove placeholder files (#15128) These were only created to mark the corresponding mathlib3 files as ported, and can safely be deleted now. commit ad0a80b0813dff599cb4f00170949b41d1c5dc5d Author: Yaël Dillies <[email protected]> Date: Fri Jul 26 12:50:24 2024 +0000 refactor: Extract predicate for conditional kernels (#15105) Sometimes conditional kernels exist "by chance" and the existing `Measure.condKernel` and `Kernel.condKernel` definitions fail to capture this. This PR extracts the disintegration property of conditional kernels into two Prop-valued typeclasses `Measure.IsCondKernel` and `Kernel.IsCondKernel`. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/github.20permission/near/453644387) Co-authored-by: Kin Yau James Wong <[email protected]> commit 0856a51f9302e460e084cffbe36d798957c107ae Author: Wojciech Nawrocki <[email protected]> Date: Fri Jul 26 12:50:22 2024 +0000 chore: bump ProofWidgets4 to v0.0.40 (#15100) Co-authored-by: Wojciech Nawrocki <[email protected]> commit 7f05fec784a8b0547074bdcf34770e46b7368e97 Author: Pim Otte <[email protected]> Date: Fri Jul 26 11:21:57 2024 +0000 feat({Algebra/BigOperators,Combinatorics/SimpleGraph}): Odd cardinality of odd components (#14623) Added lemma to prove a graph on an odd number of nodes has an odd number of odd components, including supporting lemmas. In preparation for Tuttes theorem Co-authored-by: Pim Otte <[email protected]> Co-authored-by: Yaël Dillies <[email protected]> Co-authored-by: Rida Hamadani <[email protected]> commit 75defd205f298e1b8d4197cc1b81c598f01000d6 Author: Andrew Yang <[email protected]> Date: Fri Jul 26 10:22:05 2024 +0000 feat(RingTheory): Surjective on stalks ring homomorphisms. (#14377) Co-authored-by: Andrew Yang <[email protected]> commit 3f894574d62922aa2488af6ad932a3d9b61e1d98 Author: Etienne <[email protected]> Date: Fri Jul 26 09:14:00 2024 +0000 doc: Forgotten capital letter (#15159) A capital letter was missing at the beginning of a sentence. commit 918df05c07d0801e36a7240da8a218374d26292d Author: Kim Morrison <[email protected]> Date: Fri Jul 26 09:13:58 2024 +0000 chore: robustifying for debug.byAsSorry (part 9) (#15150) See [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Running.20Mathlib.20under.20.60set_option.20debug.2EbyAsSorry.60). commit 15ce681a7cad6ea4a183d16ad5979b93ff1ec5b5 Author: Jireh Loreaux <[email protected]…
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
Found by the DecidableEq linter in #10235. Co-authored-by: Parcly Taxel <[email protected]>
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
Found by the DecidableEq linter in #10235. Co-authored-by: Parcly Taxel <[email protected]>
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 12, 2024
Found by the DecidableEq linter in #10235. Co-authored-by: Parcly Taxel <[email protected]>
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.
Found by the DecidableEq linter in #10235.