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] - refactor(topology/metric_space/isometry): generalize to pseudo_metric #6910

Closed
wants to merge 20 commits into from
Closed

[Merged by Bors] - refactor(topology/metric_space/isometry): generalize to pseudo_metric #6910

wants to merge 20 commits into from

Commits on Mar 26, 2021

  1. refactor(analysis/normed_space/basic): add semi_normed_group

    @riccardobrasca
    riccardobrasca committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    188e267 View commit details
    Browse the repository at this point in the history

  2. elaborator needs help

    @riccardobrasca
    riccardobrasca committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    5c2e33d View commit details
    Browse the repository at this point in the history

  3. I don't know why this is needed

    @riccardobrasca
    riccardobrasca committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    1a13b7e View commit details
    Browse the repository at this point in the history

  4. ring_nf not idempotent

    @riccardobrasca
    riccardobrasca committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    4afb7e9 View commit details
    Browse the repository at this point in the history

  5. elaborator needs help

    @riccardobrasca
    riccardobrasca committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    7bca0cc View commit details
    Browse the repository at this point in the history

  6. refactor(analysis/normed_space/basic): add semi_normed_ring

    @riccardobrasca
    riccardobrasca committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    e8ebb95 View commit details
    Browse the repository at this point in the history

  7. docs

    @riccardobrasca
    riccardobrasca committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    2d3d620 View commit details
    Browse the repository at this point in the history

  8. merge master

    @riccardobrasca
    riccardobrasca committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    06d2c76 View commit details
    Browse the repository at this point in the history

  9. docs

    @riccardobrasca
    riccardobrasca committed Mar 26, 2021
    Configuration menu
    Copy the full SHA
    bdd2c79 View commit details
    Browse the repository at this point in the history

Commits on Mar 27, 2021

  1. Merge branch 'master' into semi_normed_ring

    @riccardobrasca
    riccardobrasca committed Mar 27, 2021
    Configuration menu
    Copy the full SHA
    51fde35 View commit details
    Browse the repository at this point in the history

  2. refactor(topology/metric_space/isometry): generalize to pseudo_metric

    @riccardobrasca
    riccardobrasca committed Mar 27, 2021
    Configuration menu
    Copy the full SHA
    1945f91 View commit details
    Browse the repository at this point in the history

  3. elaborator needs help

    @riccardobrasca
    riccardobrasca committed Mar 27, 2021
    Configuration menu
    Copy the full SHA
    7eb8cf3 View commit details
    Browse the repository at this point in the history

Commits on Mar 28, 2021

  1. Merge branch 'master' into semi_normed_ring

    @riccardobrasca
    riccardobrasca committed Mar 28, 2021
    Configuration menu
    Copy the full SHA
    eca1a35 View commit details
    Browse the repository at this point in the history

Commits on Mar 29, 2021

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

    Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
    @riccardobrasca @semorrison
    riccardobrasca and semorrison committed Mar 29, 2021
    Configuration menu
    Copy the full SHA
    130170d View commit details
    Browse the repository at this point in the history

  2. golf

    @riccardobrasca
    riccardobrasca committed Mar 29, 2021
    Configuration menu
    Copy the full SHA
    10f5934 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'semi_normed_ring' into pseudo_isometry

    @riccardobrasca
    riccardobrasca committed Mar 29, 2021
    Configuration menu
    Copy the full SHA
    0be6801 View commit details
    Browse the repository at this point in the history

Commits on Mar 31, 2021

  1. merge master

    @riccardobrasca
    riccardobrasca committed Mar 31, 2021
    Configuration menu
    Copy the full SHA
    77e03bb View commit details
    Browse the repository at this point in the history

  2. golf

    @riccardobrasca
    riccardobrasca committed Mar 31, 2021
    Configuration menu
    Copy the full SHA
    35b82de View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2021

  1. Update src/topology/metric_space/isometry.lean 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @riccardobrasca @sgouezel
    riccardobrasca and sgouezel committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    86f4601 View commit details
    Browse the repository at this point in the history

  2. Update src/topology/metric_space/isometry.lean 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @riccardobrasca @sgouezel
    riccardobrasca and sgouezel committed Apr 2, 2021
    Configuration menu
    Copy the full SHA
    4faa983 View commit details
    Browse the repository at this point in the history