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(analysis/normed_space/enorm): define extended norm #2897

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(analysis/normed_space/enorm): define extended norm #2897

wants to merge 4 commits into from

Commits on Jun 1, 2020

  1. feat(analysis/normed_space/enorm): define extended norm

    @urkud
    urkud committed Jun 1, 2020
    Configuration menu
    Copy the full SHA
    ac4cb8b View commit details
    Browse the repository at this point in the history

Commits on Jun 2, 2020

  1. Update 

    * use `𝕜` instead of `k`;
* add `semilattice_sup_top` instance;
* make `classical.prop_dec` a high priority instance;
* more docs
    @urkud
    urkud committed Jun 2, 2020
    Configuration menu
    Copy the full SHA
    ecf4c48 View commit details
    Browse the repository at this point in the history

Commits on Jun 3, 2020

  1. Update src/analysis/normed_space/enorm.lean

    @sgouezel
    sgouezel committed Jun 3, 2020
    Configuration menu
    Copy the full SHA
    b968a1b View commit details
    Browse the repository at this point in the history

  2. Update src/analysis/normed_space/enorm.lean

    @sgouezel
    sgouezel committed Jun 3, 2020
    Configuration menu
    Copy the full SHA
    1bb5172 View commit details
    Browse the repository at this point in the history