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(ring_theory/{ideal/basic, adjoin_root): some lemmas from #15000 #16450

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(ring_theory/{ideal/basic, adjoin_root): some lemmas from #15000 #16450

wants to merge 12 commits into from

Commits on Sep 9, 2022

  1. Init

    @Paul-Lez
    Paul-Lez committed Sep 9, 2022
    Configuration menu
    Copy the full SHA
    7aef052 View commit details
    Browse the repository at this point in the history

  2. More stuff from #15000

    @Paul-Lez
    Paul-Lez committed Sep 9, 2022
    Configuration menu
    Copy the full SHA
    9b8c7b4 View commit details
    Browse the repository at this point in the history

Commits on Sep 11, 2022

  1. Fixed errors

    @Paul-Lez
    Paul-Lez committed Sep 11, 2022
    Configuration menu
    Copy the full SHA
    8f4c52f View commit details
    Browse the repository at this point in the history

Commits on Sep 12, 2022

  1. WIP

    @Paul-Lez
    Paul-Lez committed Sep 12, 2022
    Configuration menu
    Copy the full SHA
    df17856 View commit details
    Browse the repository at this point in the history

  2. Small style change

    @Paul-Lez
    Paul-Lez committed Sep 12, 2022
    Configuration menu
    Copy the full SHA
    64646af View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2022

  1. Fixed some more proofs

    @Paul-Lez
    Paul-Lez committed Sep 13, 2022
    Configuration menu
    Copy the full SHA
    e7fcfc9 View commit details
    Browse the repository at this point in the history

  2. test fix

    @Paul-Lez
    Paul-Lez committed Sep 13, 2022
    Configuration menu
    Copy the full SHA
    b308cce View commit details
    Browse the repository at this point in the history

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

    @Paul-Lez
    Paul-Lez committed Sep 13, 2022
    Configuration menu
    Copy the full SHA
    1c410ab View commit details
    Browse the repository at this point in the history

  4. Fix long line error

    @Paul-Lez
    Paul-Lez committed Sep 13, 2022
    Configuration menu
    Copy the full SHA
    d732961 View commit details
    Browse the repository at this point in the history

  5. Add simp tag to lemma

    @Paul-Lez
    Paul-Lez committed Sep 13, 2022
    Configuration menu
    Copy the full SHA
    2a8b066 View commit details
    Browse the repository at this point in the history

Commits on Sep 14, 2022

  1. Remove simp tag from problematic lemma

    @Paul-Lez
    Paul-Lez committed Sep 14, 2022
    Configuration menu
    Copy the full SHA
    11fd0f9 View commit details
    Browse the repository at this point in the history

  2. Remove another simp lemma

    @Paul-Lez
    Paul-Lez committed Sep 14, 2022
    Configuration menu
    Copy the full SHA
    3bd9cea View commit details
    Browse the repository at this point in the history