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

[Merged by Bors] - refactor: generalize SMul (Ideal R) (Submodule R M) to SMul (Submodule R A) (Submodule R M) #18419

Closed
wants to merge 32 commits into from
Closed

[Merged by Bors] - refactor: generalize SMul (Ideal R) (Submodule R M) to SMul (Submodule R A) (Submodule R M) #18419

wants to merge 32 commits into from

Commits on Oct 14, 2024

  1. refactor: generalize mul of Submodule and smul of Ideal on Submodule … 

    …to noncommutative setting
    @alreadydone
    alreadydone committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    94d510a View commit details
    Browse the repository at this point in the history

  2. Discard changes to Mathlib/RingTheory/JacobsonIdeal.lean

    @alreadydone
    alreadydone committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    c31a232 View commit details
    Browse the repository at this point in the history

  3. fixes

    @alreadydone
    alreadydone committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    71046e2 View commit details
    Browse the repository at this point in the history

  4. fixes

    @alreadydone
    alreadydone committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    fb0536c View commit details
    Browse the repository at this point in the history

  5. fixes

    @alreadydone
    alreadydone committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    3cbb1e9 View commit details
    Browse the repository at this point in the history

  6. fixes

    @alreadydone
    alreadydone committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    810908a View commit details
    Browse the repository at this point in the history

  7. fixes

    @alreadydone
    alreadydone committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    0c22392 View commit details
    Browse the repository at this point in the history

  8. fixes

    @alreadydone
    alreadydone committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    2af93ae View commit details
    Browse the repository at this point in the history

  9. missing docstring

    @alreadydone
    alreadydone authored Oct 14, 2024
    Configuration menu
    Copy the full SHA
    e3e517d View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2024

  1. Merge branch 'master' into Ideal.mul

    @alreadydone
    alreadydone authored Oct 18, 2024
    Configuration menu
    Copy the full SHA
    1fcc086 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into Ideal.mul

    @alreadydone
    alreadydone authored Oct 18, 2024
    Configuration menu
    Copy the full SHA
    913d508 View commit details
    Browse the repository at this point in the history

  3. fixes

    @alreadydone
    alreadydone committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    ff7e3bb View commit details
    Browse the repository at this point in the history

Commits on Oct 24, 2024

  1. Merge branch 'master' into Ideal.mul

    @alreadydone
    alreadydone authored Oct 24, 2024
    Configuration menu
    Copy the full SHA
    74c5fbf View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into Ideal.mul

    @alreadydone
    alreadydone authored Oct 24, 2024
    Configuration menu
    Copy the full SHA
    b8032bc View commit details
    Browse the repository at this point in the history

Commits on Oct 26, 2024

  1. Merge branch 'master' into Ideal.mul

    @alreadydone
    alreadydone authored Oct 26, 2024
    Configuration menu
    Copy the full SHA
    1751a4d View commit details
    Browse the repository at this point in the history

  2. fixes

    @alreadydone
    alreadydone committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    54e02d4 View commit details
    Browse the repository at this point in the history

Commits on Oct 27, 2024

  1. refactor: generalize AddSubmonoid Mul lemmas to SMul

    @alreadydone
    alreadydone committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    b6a7eb9 View commit details
    Browse the repository at this point in the history

  2. golf Ideal/Operations using the SMul lemmas

    @alreadydone
    alreadydone committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    b0ba705 View commit details
    Browse the repository at this point in the history

  3. fix + minigolfs

    @alreadydone
    alreadydone committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    62c1fa9 View commit details
    Browse the repository at this point in the history

  4. minigolfs

    @alreadydone
    alreadydone committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    5e67fb1 View commit details
    Browse the repository at this point in the history

  5. get rid of large-import

    @alreadydone
    alreadydone committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    fe39874 View commit details
    Browse the repository at this point in the history

Commits on Oct 28, 2024

  1. Merge branch 'master' into Ideal.mul

    @alreadydone
    alreadydone authored Oct 28, 2024
    Configuration menu
    Copy the full SHA
    ff411cc View commit details
    Browse the repository at this point in the history

  2. reduce diff

    @alreadydone
    alreadydone authored Oct 28, 2024
    Configuration menu
    Copy the full SHA
    9f9c59d View commit details
    Browse the repository at this point in the history

  3. revert

    @alreadydone
    alreadydone committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    97f5e9a View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2024

  1. generalize to SMul (Submodule R A) (Submodule R M)

    @alreadydone
    alreadydone committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    e5fd5d6 View commit details
    Browse the repository at this point in the history

Commits on Oct 30, 2024

  1. fix

    @alreadydone
    alreadydone committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    46cd376 View commit details
    Browse the repository at this point in the history

  2. fix

    @alreadydone
    alreadydone committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    8cabc5f View commit details
    Browse the repository at this point in the history

  3. minor

    @alreadydone
    alreadydone authored Oct 30, 2024
    Configuration menu
    Copy the full SHA
    5f8fc87 View commit details
    Browse the repository at this point in the history

Commits on Nov 8, 2024

  1. Merge branch 'master' into Submodule.SMul

    @alreadydone
    alreadydone authored Nov 8, 2024
    Configuration menu
    Copy the full SHA
    6546fad View commit details
    Browse the repository at this point in the history

Commits on Dec 3, 2024

  1. Merge pull request #19706 from leanprover-community/master

    @alreadydone
    alreadydone authored Dec 3, 2024
    Configuration menu
    Copy the full SHA
    09ec416 View commit details
    Browse the repository at this point in the history

  2. move lemma

    @alreadydone
    alreadydone committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    d3c5b98 View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2024

  1. Merge branch 'master' into Submodule.SMul

    @alreadydone
    alreadydone authored Dec 4, 2024
    Configuration menu
    Copy the full SHA
    efe2593 View commit details
    Browse the repository at this point in the history