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] - refactor(ring_theory/ideal/*, ring_theory/jacobson): use comm_semiring instead of comm_ring for ideals #5954

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - refactor(ring_theory/ideal/*, ring_theory/jacobson): use comm_semiring instead of comm_ring for ideals #5954

wants to merge 16 commits into from

Commits on Jan 27, 2021

  1. start using comm_semiring in ideal

    @adomani
    adomani committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    af91307 View commit details
    Browse the repository at this point in the history

  2. fix algebra/ring_quot

    @adomani
    adomani committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    5c99415 View commit details
    Browse the repository at this point in the history

  3. fix ring_theory/jacobson_ideal

    @adomani
    adomani committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    e1c73cd View commit details
    Browse the repository at this point in the history

  4. remove temporary file

    @adomani
    adomani committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    b796475 View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2021

  1. fix ring_theory/jacobson

    @adomani
    adomani committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    a432356 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of github.com:leanprover-community/mathlib into… 

    … semi_ideals
    @adomani
    adomani committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    3f9e0c7 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' of github.com:leanprover-community/mathlib into… 

    … semi_ideals
    @adomani
    adomani committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    9c04b60 View commit details
    Browse the repository at this point in the history

  4. cleaning up

    @adomani
    adomani committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    da02236 View commit details
    Browse the repository at this point in the history

  5. add module doc-strings

    @adomani
    adomani committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    d198c17 View commit details
    Browse the repository at this point in the history

  6. move three lemmas to ring_theory/ideal/over 

    clean up
    @adomani
    adomani committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    d8bd499 View commit details
    Browse the repository at this point in the history

  7. Update src/algebra/ring_quot.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @adomani @eric-wieser
    adomani and eric-wieser committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    e09e0d6 View commit details
    Browse the repository at this point in the history

  8. Update src/ring_theory/ideal/over.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @adomani @eric-wieser
    adomani and eric-wieser committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    da22901 View commit details
    Browse the repository at this point in the history

  9. Update src/ring_theory/ideal/basic.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @adomani @eric-wieser
    adomani and eric-wieser committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    26b66af View commit details
    Browse the repository at this point in the history

  10. Update src/ring_theory/ideal/basic.lean 

    Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
    @adomani @XavierXarles
    adomani and XavierXarles committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    0360340 View commit details
    Browse the repository at this point in the history

  11. Update src/ring_theory/ideal/basic.lean 

    Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
    @adomani @XavierXarles
    adomani and XavierXarles committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    3271184 View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2021

  1. Apply Bryan's suggestions from code review 

    Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
    @adomani @bryangingechen
    adomani and bryangingechen committed Feb 1, 2021
    Configuration menu
    Copy the full SHA
    b0d1dcd View commit details
    Browse the repository at this point in the history