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(algebra/ring_quot): quotients of noncommutative rings #4078

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - feat(algebra/ring_quot): quotients of noncommutative rings #4078

wants to merge 21 commits into from

Commits on Sep 8, 2020

  1. quotients of noncommutative rings

    @semorrison
    semorrison committed Sep 8, 2020
    Configuration menu
    Copy the full SHA
    69fb2d7 View commit details
    Browse the repository at this point in the history

  2. first cut

    @semorrison
    semorrison committed Sep 8, 2020
    Configuration menu
    Copy the full SHA
    fee007d View commit details
    Browse the repository at this point in the history

  3. comment

    @semorrison
    semorrison committed Sep 8, 2020
    Configuration menu
    Copy the full SHA
    ed2853c View commit details
    Browse the repository at this point in the history

  4. fix

    @semorrison
    semorrison committed Sep 8, 2020
    Configuration menu
    Copy the full SHA
    b5724e5 View commit details
    Browse the repository at this point in the history

  5. fix

    @semorrison
    semorrison committed Sep 8, 2020
    Configuration menu
    Copy the full SHA
    920503e View commit details
    Browse the repository at this point in the history

Commits on Sep 11, 2020

  1. use case

    @semorrison
    semorrison committed Sep 11, 2020
    Configuration menu
    Copy the full SHA
    c60e8eb View commit details
    Browse the repository at this point in the history

Commits on Sep 14, 2020

  1. Update src/algebra/ring_quot.lean 

    Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
    @semorrison @kckennylau
    semorrison and kckennylau committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    c67f886 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into ring_quot

    @semorrison
    semorrison committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    e3d47c7 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'ring_quot' of github.com:leanprover-community/mathlib i… 

    …nto ring_quot
    @semorrison
    semorrison committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    fca07ba View commit details
    Browse the repository at this point in the history

  4. merge/fix

    @semorrison
    semorrison committed Sep 14, 2020
    Configuration menu
    Copy the full SHA
    40f33fd View commit details
    Browse the repository at this point in the history

Commits on Sep 15, 2020

  1. Apply suggestions from code review 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @semorrison @eric-wieser
    semorrison and eric-wieser committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    741a32f View commit details
    Browse the repository at this point in the history

  2. get things working again

    @semorrison
    semorrison committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    d51ae36 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into ring_quot

    @semorrison
    semorrison committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    86c169b View commit details
    Browse the repository at this point in the history

  4. change apply lemma so it's actually about an application

    @semorrison
    semorrison committed Sep 15, 2020
    Configuration menu
    Copy the full SHA
    56e3061 View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2020

  1. merge

    @semorrison
    semorrison committed Sep 16, 2020
    Configuration menu
    Copy the full SHA
    932e0c3 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @semorrison @eric-wieser
    semorrison and eric-wieser committed Sep 16, 2020
    Configuration menu
    Copy the full SHA
    b60a072 View commit details
    Browse the repository at this point in the history

  3. missing doc-string

    @semorrison
    semorrison committed Sep 16, 2020
    Configuration menu
    Copy the full SHA
    55b4174 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'ring_quot' of github.com:leanprover-community/mathlib i… 

    …nto ring_quot
    @semorrison
    semorrison committed Sep 16, 2020
    Configuration menu
    Copy the full SHA
    8f8cca3 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/master' into ring_quot

    @semorrison
    semorrison committed Sep 16, 2020
    Configuration menu
    Copy the full SHA
    740914e View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2020

  1. fixes

    @semorrison
    semorrison committed Sep 17, 2020
    Configuration menu
    Copy the full SHA
    4928281 View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2020

  1. use 'case' tactic

    @semorrison
    semorrison committed Sep 19, 2020
    Configuration menu
    Copy the full SHA
    6c96a88 View commit details
    Browse the repository at this point in the history