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/Submonoid/Basic #1224

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat: port GroupTheory/Submonoid/Basic #1224

wants to merge 9 commits into from

Commits on Dec 26, 2022

  1. Initial Commit

    @ADedecker
    ADedecker committed Dec 26, 2022
    Configuration menu
    Copy the full SHA
    626142a View commit details
    Browse the repository at this point in the history

  2. Should be done

    @ADedecker
    ADedecker committed Dec 26, 2022
    Configuration menu
    Copy the full SHA
    5568a10 View commit details
    Browse the repository at this point in the history

  3. Porting note

    @ADedecker
    ADedecker committed Dec 26, 2022
    Configuration menu
    Copy the full SHA
    3bb2289 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/GroupTheory/Submonoid/Basic.lean 

    Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
    @ADedecker @ChrisHughes24
    ADedecker and ChrisHughes24 committed Dec 26, 2022
    Configuration menu
    Copy the full SHA
    0d9b14c View commit details
    Browse the repository at this point in the history

Commits on Dec 28, 2022

  1. Fix slow

    @ADedecker
    ADedecker committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    3017cf4 View commit details
    Browse the repository at this point in the history

  2. Add M back?

    @ADedecker
    ADedecker committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    22323d6 View commit details
    Browse the repository at this point in the history

  3. Minor updates

    @urkud
    urkud committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    12d6051 View commit details
    Browse the repository at this point in the history

  4. Fix lint

    @ADedecker
    ADedecker committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    edf7a6f View commit details
    Browse the repository at this point in the history

  5. Merge branch 'AD_PORT_Submonoid_Basic' of github.com:leanprover-commu… 

    …nity/mathlib4 into AD_PORT_Submonoid_Basic
    @ADedecker
    ADedecker committed Dec 28, 2022
    Configuration menu
    Copy the full SHA
    ada60be View commit details
    Browse the repository at this point in the history