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: port GroupTheory.Subgroup.Basic #1797

Closed
wants to merge 37 commits into from
Closed

[Merged by Bors] - feat: port GroupTheory.Subgroup.Basic #1797

wants to merge 37 commits into from

Commits on Jan 23, 2023

  1. feat: port GroupTheory.Subgroup.Basic

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Jan 23, 2023
    Configuration menu
    Copy the full SHA
    d17ef23 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Jan 23, 2023
    Configuration menu
    Copy the full SHA
    853951a View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @Ruben-VandeVelde
    Ruben-VandeVelde committed Jan 23, 2023
    Configuration menu
    Copy the full SHA
    389e6a7 View commit details
    Browse the repository at this point in the history

  4. fixes

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Jan 23, 2023
    Configuration menu
    Copy the full SHA
    b7d6afc View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2023

  1. minifix

    @jcommelin
    jcommelin committed Jan 24, 2023
    Configuration menu
    Copy the full SHA
    0b6c65c View commit details
    Browse the repository at this point in the history

  2. give hasZsmul and hasZpow congruent types

    @LukasMias
    LukasMias committed Jan 24, 2023
    Configuration menu
    Copy the full SHA
    b41d249 View commit details
    Browse the repository at this point in the history

  3. small fixes

    @LukasMias
    LukasMias committed Jan 24, 2023
    Configuration menu
    Copy the full SHA
    7738cf5 View commit details
    Browse the repository at this point in the history

Commits on Jan 25, 2023

  1. Fixed comments and more.

    @qawbecrdtey
    qawbecrdtey committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    0b9029c View commit details
    Browse the repository at this point in the history

  2. More fixes.

    @qawbecrdtey
    qawbecrdtey committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    7714bdf View commit details
    Browse the repository at this point in the history

  3. further changes

    @LukasMias
    LukasMias committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    4ba794d View commit details
    Browse the repository at this point in the history

  4. Fix simps projection

    @Vierkantor
    Vierkantor committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    4d9390c View commit details
    Browse the repository at this point in the history

  5. Use simp because the triangle is being obstinate again

    @Vierkantor
    Vierkantor committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    1008741 View commit details
    Browse the repository at this point in the history

  6. Fix many of the typeclass issues: unbundled subclasses of outParam … 

    …classes should not repeat the parents' `outParam`
    @Vierkantor
    Vierkantor committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    b8ca528 View commit details
    Browse the repository at this point in the history

  7. docstrings & minor fixes

    @LukasMias
    LukasMias committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    faf49b1 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'port/GroupTheory.Subgroup.Basic' of github.com:leanprov… 

    …er-community/mathlib4 into port/GroupTheory.Subgroup.Basic
    @LukasMias
    LukasMias committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    0bf9024 View commit details
    Browse the repository at this point in the history

  9. long lines

    @LukasMias
    LukasMias committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    04f7e2b View commit details
    Browse the repository at this point in the history

  10. restore Subgroup.inclusion

    @LukasMias
    LukasMias committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    e3db17b View commit details
    Browse the repository at this point in the history

  11. some redundant arguments

    @LukasMias
    LukasMias committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    8923ba1 View commit details
    Browse the repository at this point in the history

  12. Merge remote-tracking branch 'origin/master' into port/GroupTheory.Su… 

    …bgroup.Basic
    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    6dbfc29 View commit details
    Browse the repository at this point in the history

  13. minifix

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    e604b3b View commit details
    Browse the repository at this point in the history

  14. fix some errors

    @fpvandoorn
    fpvandoorn committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    af42022 View commit details
    Browse the repository at this point in the history

  15. change instance names

    @fpvandoorn
    fpvandoorn committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    7f152a1 View commit details
    Browse the repository at this point in the history

  16. fixes

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    600b4fa View commit details
    Browse the repository at this point in the history

  17. fixes

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    73e8a0f View commit details
    Browse the repository at this point in the history

  18. fixes

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    7e73377 View commit details
    Browse the repository at this point in the history

  19. fixes

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    5f85930 View commit details
    Browse the repository at this point in the history

  20. fixes

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    faba79d View commit details
    Browse the repository at this point in the history

  21. auto: fix lints

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    81ffc4e View commit details
    Browse the repository at this point in the history

  22. auto: naming

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    718cd39 View commit details
    Browse the repository at this point in the history

  23. fix long lines

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    ec16bef View commit details
    Browse the repository at this point in the history

  24. fix a lint

    @jcommelin
    jcommelin committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    db40de4 View commit details
    Browse the repository at this point in the history

  25. fix remaining errors, add porting note

    @fpvandoorn
    fpvandoorn committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    0953d4e View commit details
    Browse the repository at this point in the history

  26. Merge remote-tracking branch 'origin/port/GroupTheory.Subgroup.Basic'… 

    … into port/GroupTheory.Subgroup.Basic
    @fpvandoorn
    fpvandoorn committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    651f7b8 View commit details
    Browse the repository at this point in the history

  27. lintfixes

    @fpvandoorn
    fpvandoorn committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    74c8a00 View commit details
    Browse the repository at this point in the history

  28. fix

    @fpvandoorn
    fpvandoorn committed Jan 25, 2023
    Configuration menu
    Copy the full SHA
    a59af1b View commit details
    Browse the repository at this point in the history

Commits on Jan 26, 2023

  1. Apply suggestions from code review

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    c12a653 View commit details
    Browse the repository at this point in the history

  2. to_additive some simps

    @ChrisHughes24
    ChrisHughes24 committed Jan 26, 2023
    Configuration menu
    Copy the full SHA
    7d4c9e7 View commit details
    Browse the repository at this point in the history