Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: define logarithmic derivatives #12804

Closed
wants to merge 50 commits into from
Closed

[Merged by Bors] - feat: define logarithmic derivatives #12804

wants to merge 50 commits into from

Conversation

CBirkbeck
Copy link
Collaborator

@CBirkbeck CBirkbeck commented May 10, 2024 •
edited
Loading

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.

Open in Gitpod

@grunweg grunweg added WIP Work in progress t-analysis Analysis (normed *, calculus) labels May 24, 2024
@CBirkbeck CBirkbeck changed the title WIP logarithmic derivatives Define logarithmic derivatives May 27, 2024
@CBirkbeck CBirkbeck marked this pull request as ready for review May 27, 2024 13:41
@CBirkbeck CBirkbeck removed the WIP Work in progress label May 27, 2024
@CBirkbeck CBirkbeck added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label May 27, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 26, 2024
@urkud urkud added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 27, 2024
@urkud
Copy link
Member

urkud commented Jul 27, 2024

Otherwise LGTM. Thanks!

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 27, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 29, 2024
@CBirkbeck
Copy link
Collaborator Author

CBirkbeck commented Jul 29, 2024 •
edited
Loading

Thanks for the golf/cleanup! I've made the suggested changes and removed the now obsolete files.

@urkud
Copy link
Member

urkud commented Jul 29, 2024

Next time please remove the awaiting-author label once the PR is ready for another review.

@urkud urkud removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 29, 2024
@urkud
Copy link
Member

urkud commented Jul 29, 2024

Thanks! Once CI is happy, please merge this PR using bors r+
bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 29, 2024

✌️ CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@urkud
Copy link
Member

urkud commented Jul 29, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 29, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 29, 2024
@CBirkbeck @urkud
feat: define logarithmic derivatives (#12804)
4196dc8 
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]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 29, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: define logarithmic derivatives [Merged by Bors] - feat: define logarithmic derivatives Jul 29, 2024
@mathlib-bors mathlib-bors bot closed this Jul 29, 2024
@mathlib-bors mathlib-bors bot deleted the logarithmic_derivatives branch July 29, 2024 18:07
Rida-Hamadani pushed a commit that referenced this pull request Jul 29, 2024
@CBirkbeck @urkud @Rida-Hamadani
feat: define logarithmic derivatives (#12804)
6ea738c 
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]>
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Rida-Hamadani added a commit that referenced this pull request Aug 3, 2024
@Rida-Hamadani
Squashed commit of the following:
003ef41 
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]…
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@Ruben-VandeVelde Ruben-VandeVelde Awaiting requested review from Ruben-VandeVelde

Assignees

@urkud urkud

Labels
delegated ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@CBirkbeck @leanprover-community-mathlib4-bot @urkud @Ruben-VandeVelde @kim-em @grunweg @YaelDillies