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

feat: basic results about the differentiability of the norm #17150

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

feat: basic results about the differentiability of the norm #17150

wants to merge 6 commits into from
+193 −1

Commits on Sep 26, 2024

  1. feat: basic results about the differentiability of the norm

    Etienne Marion committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    2cc8e91 View commit details
    Browse the repository at this point in the history

  2. update Mathlib.lean

    Etienne Marion committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    66205f0 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2024

  1. Merge remote-tracking branch 'origin/master' into em/deriv_norm

    Etienne Marion committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    7d6513c View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2024

  1. add more API

    Etienne Marion committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    538e47b View commit details
    Browse the repository at this point in the history

  2. useless variables

    Etienne Marion committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    60e712b View commit details
    Browse the repository at this point in the history

  3. golf

    Etienne Marion committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    a25518b View commit details
    Browse the repository at this point in the history