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 Algebra.Category.GroupWithZero #3962

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat: port Algebra.Category.GroupWithZero #3962

wants to merge 15 commits into from

Commits on May 13, 2023

  1. feat: port Algebra.Category.GroupWithZero

    Pim Otte committed May 13, 2023
    Configuration menu
    Copy the full SHA
    e0afd8d View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    Pim Otte committed May 13, 2023
    Configuration menu
    Copy the full SHA
    9d5f555 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
    Pim Otte committed May 13, 2023
    Configuration menu
    Copy the full SHA
    692c9ea View commit details
    Browse the repository at this point in the history

Commits on May 14, 2023

  1. wip

    Pim Otte committed May 14, 2023
    Configuration menu
    Copy the full SHA
    702364d View commit details
    Browse the repository at this point in the history

  2. Solve FunLike coercion

    Pim Otte committed May 14, 2023
    Configuration menu
    Copy the full SHA
    fad1376 View commit details
    Browse the repository at this point in the history

Commits on May 18, 2023

  1. Fixes

    Pim Otte committed May 18, 2023
    Configuration menu
    Copy the full SHA
    bd5a2cb View commit details
    Browse the repository at this point in the history

  2. Lint fixes

    Pim Otte committed May 18, 2023
    Configuration menu
    Copy the full SHA
    a9938f2 View commit details
    Browse the repository at this point in the history

  3. Lint fixes

    Pim Otte committed May 18, 2023
    Configuration menu
    Copy the full SHA
    99150d3 View commit details
    Browse the repository at this point in the history

  4. Comment fixes

    Pim Otte committed May 18, 2023
    Configuration menu
    Copy the full SHA
    c6ca4ab View commit details
    Browse the repository at this point in the history

  5. Name fixes

    Pim Otte committed May 18, 2023
    Configuration menu
    Copy the full SHA
    09e7cf8 View commit details
    Browse the repository at this point in the history

Commits on May 20, 2023

  1. Write out simp

    Pim Otte committed May 20, 2023
    Configuration menu
    Copy the full SHA
    3b55178 View commit details
    Browse the repository at this point in the history

Commits on May 22, 2023

  1. Apply suggestions from code review 

    Co-authored-by: Scott Morrison <scott@tqft.net>
    @semorrison
    Pim Otte and semorrison committed May 22, 2023
    Configuration menu
    Copy the full SHA
    4cbc50a View commit details
    Browse the repository at this point in the history

  2. More code review fixes

    Pim Otte committed May 22, 2023
    Configuration menu
    Copy the full SHA
    ca77a4e View commit details
    Browse the repository at this point in the history

  3. Add Cat to filename for consitency

    Pim Otte committed May 22, 2023
    Configuration menu
    Copy the full SHA
    e217732 View commit details
    Browse the repository at this point in the history

  4. Fix Mathlib.lean

    Pim Otte committed May 22, 2023
    Configuration menu
    Copy the full SHA
    cef81a8 View commit details
    Browse the repository at this point in the history