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: finite products/sums of differentiable maps into smooth commutative monoids are differentiable #9775

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat: finite products/sums of differentiable maps into smooth commutative monoids are differentiable #9775

wants to merge 14 commits into from

Commits on Jan 15, 2024

  1. Add some docstrings.

    @grunweg
    grunweg committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    4b5ef7c View commit details
    Browse the repository at this point in the history

  2. Tweak section names, add comments explaining them.

    @grunweg
    grunweg committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    23a1d27 View commit details
    Browse the repository at this point in the history

  3. Main doc: reflow lines.

    @grunweg
    grunweg committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    31e3be5 View commit details
    Browse the repository at this point in the history

  4. Extend main module docstring.

    @grunweg
    grunweg committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    ff339e4 View commit details
    Browse the repository at this point in the history

Commits on Jan 16, 2024

  1. Review comments: extend documentation.

    @grunweg
    grunweg committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    b4198a5 View commit details
    Browse the repository at this point in the history

  2. Split main definitions and results; clarify additive vs multiplicativ… 

    …e Lie groups.
    @grunweg
    grunweg committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    fda1584 View commit details
    Browse the repository at this point in the history

  3. Point to other instance.

    @grunweg
    grunweg committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    3001890 View commit details
    Browse the repository at this point in the history

  4. Snapshot.

    @grunweg
    grunweg committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    ad94f27 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into MR-sphere-eversion-LieGroup2

    @grunweg
    grunweg committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    037fcda View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2024

  1. Move to Monoid file.

    @grunweg
    grunweg committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    914399c View commit details
    Browse the repository at this point in the history

  2. chore: re-order lemmas into logical order. 

    group as contMDiffWithAt, contMDiffAt, contMDiffOn, contMDiff;
smoothWithinAt, smoothAt, smoothOn, smooth

In each group, there are prod, finprod, finset_prod, finset_prod' lemmas.

This commit is purely code motion.
    @grunweg
    grunweg committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    6e44518 View commit details
    Browse the repository at this point in the history

  3. Open Function for mulSupport.

    @grunweg
    grunweg committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    64056c1 View commit details
    Browse the repository at this point in the history

  4. Small golf; add contMDiffOn_finprod.

    @grunweg
    grunweg committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    1a668f6 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

    @ocfnash
    ocfnash committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    acb4ed5 View commit details
    Browse the repository at this point in the history