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

sync to master #17157

Merged
merged 9 commits into from
Sep 26, 2024
Merged

sync to master #17157

merged 9 commits into from
Sep 26, 2024

Commits on Sep 26, 2024

  1. chore: update Mathlib dependencies 2024-09-25 (#17143) 

    This PR updates the Mathlib dependencies.
    @mathlib-bors
    mathlib-bors[bot] committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    4e3fd1a View commit details
    Browse the repository at this point in the history

  2. feat: generalize normed instances on UniformSpace.Completion (#17059) 

    Notably, `NormedSpace.to_uniformContinuousConstSMul` is generalized to `BoundedSMul` on `PseudoMetricSpace`s, relaxing the scalar considerably from normed fields.



Co-authored-by: Eric Wieser <efw@google.com>
    @eric-wieser
    eric-wieser and eric-wieser committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    3874c4e View commit details
    Browse the repository at this point in the history

  3. chore: split Algebra.Bounds and Algebra.Order.Pointwise (#16986) 

    Delete `Algebra.Bounds` and `Algebra.Order.Pointwise`. Create
* `Algebra.Order.Field.Pointwise` for lemmas about pointwise operations in linear ordered fields
* `Algebra.Order.Group.CompleteLattice` for distributivity of group operations over supremum/infimum
* `Algebra.Order.Group.Pointwise.Bounds` for boundedness of pointwise-defined sets
* `Algebra.Order.Group.Pointwise.CompleteLattice` for lemmas about the supremum/infimum of pointwise-defined sets.
    @YaelDillies
    YaelDillies committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    9678fd7 View commit details
    Browse the repository at this point in the history

  4. feat(CategoryTheory): the internal hom with the monoidal unit is the … 

    …identity (#17065)

In a closed monoidal category, the internal hom defined by mapping out of the monoidal unit is naturally isomorphic to the identity. This specializes to an analogous result about exponentiating with the terminal object in a cartesian closed category.

Co-authored-by: [Dagur Asgeirsson](https://github.com/dagurtomas)
    @emilyriehl
    emilyriehl committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    3488c1c View commit details
    Browse the repository at this point in the history

  5. feat: monotonicity lemmas for OrdinalApprox (#15522) 

    This PR adds two lemmas about monotonicity for `lfpApprox` and `gfpApprox` each. I found them helpful when working with the API.



Co-authored-by: Ira Fesefeldt <public@feuervogel.me>
Co-authored-by: Ira Fesefeldt <9974411+PhoenixIra@users.noreply.github.com>
    @PhoenixIra
    3 people committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    b272ab8 View commit details
    Browse the repository at this point in the history

  6. feat(LinearAlgebra/Matrix): Woodbury Identity (#16325) 

    This adds the [Woodbury Identity](https://en.wikipedia.org/wiki/Woodbury_matrix_identity).

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Woodbury.20identity/near/462245284)

Also corrects some bad deprecations introduced in #16590, which affected development of this PR.

Co-authored-by: Mohanad Ahmad



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @4hma4d @eric-wieser
    4hma4d and eric-wieser committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    facf1f9 View commit details
    Browse the repository at this point in the history

  7. chore: fix type class assumptions for NonUnitalStarAlgHom.map_cfcₙ (#… 

    …17111)
    @j-loreaux
    j-loreaux committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    c52d5a9 View commit details
    Browse the repository at this point in the history

  8. ci: add --nightlysha to create-adaptation-pr.sh (#17148)

    @jcommelin
    jcommelin committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    78a0b2f View commit details
    Browse the repository at this point in the history

  9. chore: rename AnalyticOn to AnalyticOnNhd, and AnalyticWithinOn… 

    … to `AnalyticOn` (#17146)

For coherence with `ContinuousOn`, `DifferentiableOn` and so on. See Zulip https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/Integrate.20analytic.20functions.20in.20the.20smooth.20hierarchy/near/471899268

This is 90% renaming all `AnalyticOn` to `AnalyticOnNhd` and then `AnalyticWithinOn` to `AnalyticOn`, and then adding deprecations. The 10% remaining is, when adding a deprecation `alias AnalyticOn.foo := AnalyticOnNhd.foo`, I noticed that `AnalyticOn.foo` would definitely make sense (with the new meaning of `AnalyticOn`), so I added the lemma with the new meaning instead of deprecating the old one.
    @sgouezel
    sgouezel committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    5d4532a View commit details
    Browse the repository at this point in the history