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/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals #16446

Closed
wants to merge 27 commits into from
Closed

[Merged by Bors] - feat(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals #16446

wants to merge 27 commits into from

Commits on Sep 4, 2022

  1. initial proof of completeness

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    9f5730b View commit details
    Browse the repository at this point in the history

  2. remove commutativity requirement

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    a63714d View commit details
    Browse the repository at this point in the history

  3. remove filter.has_basis.mul

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    0645ab7 View commit details
    Browse the repository at this point in the history

  4. clean up until completeness

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    a537cdf View commit details
    Browse the repository at this point in the history

  5. clean up and add docstrings

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    2556c14 View commit details
    Browse the repository at this point in the history

  6. closed not necessary

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    0d55d8f View commit details
    Browse the repository at this point in the history

  7. More cleaning

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    3f458b1 View commit details
    Browse the repository at this point in the history

  8. simplify proof of cauchy

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    eaefdb4 View commit details
    Browse the repository at this point in the history

  9. remove inverse bits, no longer necessary

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    f239bc2 View commit details
    Browse the repository at this point in the history

  10. use filter.has_basis.cauchy_seq_iff

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    be35831 View commit details
    Browse the repository at this point in the history

  11. un-capitalize

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    4d7fd1e View commit details
    Browse the repository at this point in the history

  12. fix variables

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    8ae8dbd View commit details
    Browse the repository at this point in the history

  13. fix to_additive docstrings

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    e7f1e16 View commit details
    Browse the repository at this point in the history

  14. rename file

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    f333290 View commit details
    Browse the repository at this point in the history

  15. add module docstring and copyright

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    374adee View commit details
    Browse the repository at this point in the history

  16. generalize to arbitrary topological groups

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    f81ba8f View commit details
    Browse the repository at this point in the history

  17. fix broken norm instance

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    4325272 View commit details
    Browse the repository at this point in the history

  18. remove uniformity countably generated

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    363c7fa View commit details
    Browse the repository at this point in the history

  19. distribute to appropriate files

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    e46cf83 View commit details
    Browse the repository at this point in the history

  20. add references

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    337a9b0 View commit details
    Browse the repository at this point in the history

  21. fix Misc to Book

    @j-loreaux
    j-loreaux committed Sep 4, 2022
    Configuration menu
    Copy the full SHA
    6aa9936 View commit details
    Browse the repository at this point in the history

Commits on Sep 7, 2022

  1. use filter.has_antitone_basis.subbasis_with_rel

    @j-loreaux
    j-loreaux committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    556c93f View commit details
    Browse the repository at this point in the history

  2. add maximal ideal closed

    @j-loreaux
    j-loreaux committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    a873e3b View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2022

  1. add normed structures on quotients

    @j-loreaux
    j-loreaux committed Sep 9, 2022
    Configuration menu
    Copy the full SHA
    9fe2092 View commit details
    Browse the repository at this point in the history

  2. Revert "add maximal ideal closed" 

    This reverts commit a873e3b.
    @j-loreaux
    j-loreaux committed Sep 9, 2022
    Configuration menu
    Copy the full SHA
    71e3203 View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2022

  1. Merge branch 'master' into j-loreaux/normed-ring-quotient

    @j-loreaux
    j-loreaux committed Sep 13, 2022
    Configuration menu
    Copy the full SHA
    07afeec View commit details
    Browse the repository at this point in the history

Commits on Sep 15, 2022

  1. add a bit to the module docstring

    @j-loreaux
    j-loreaux committed Sep 15, 2022
    Configuration menu
    Copy the full SHA
    316ef79 View commit details
    Browse the repository at this point in the history