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/dedekind_domain/ideal): construct map between the sets of prime factors of ideal I and J induced by an isomorphism between R/I and S/J #16455

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal I and J induced by an isomorphism between R/I and S/J #16455

wants to merge 8 commits into from

Commits on Sep 9, 2022

  1. Init

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

Commits on Sep 10, 2022

  1. Make parameter implicit

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

  2. Fix proof

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

  3. Fix style

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

Commits on Sep 12, 2022

  1. Added projection lemmas for normalized_factors_equiv_of_quot_equiv

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

  2. Fix long line error

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

  3. Removed projection lemmas and added simps apply

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

  4. Add simp tag to lemma

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