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/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API #14656

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(ring_theory/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API #14656

wants to merge 17 commits into from

Commits on Jun 9, 2022

  1. defs

    @mckoen
    mckoen committed Jun 9, 2022
    Configuration menu
    Copy the full SHA
    001e35b View commit details
    Browse the repository at this point in the history

  2. simps

    @mckoen
    mckoen committed Jun 9, 2022
    Configuration menu
    Copy the full SHA
    ed69042 View commit details
    Browse the repository at this point in the history

  3. lemma

    @mckoen
    mckoen committed Jun 9, 2022
    Configuration menu
    Copy the full SHA
    4145d1b View commit details
    Browse the repository at this point in the history

  4. comment

    @mckoen
    mckoen committed Jun 9, 2022
    Configuration menu
    Copy the full SHA
    6ea8652 View commit details
    Browse the repository at this point in the history

Commits on Jun 10, 2022

  1. update lemma

    @mckoen
    mckoen committed Jun 10, 2022
    Configuration menu
    Copy the full SHA
    8b220a2 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'valuation_maximal' of https://github.com/leanprover-com… 

    …munity/mathlib into valuation_maximal
    @mckoen
    mckoen committed Jun 10, 2022
    Configuration menu
    Copy the full SHA
    3eb2447 View commit details
    Browse the repository at this point in the history

Commits on Jun 15, 2022

  1. changed maximal ideal to nonunits

    @mckoen
    mckoen committed Jun 15, 2022
    Configuration menu
    Copy the full SHA
    9687b52 View commit details
    Browse the repository at this point in the history

Commits on Jun 22, 2022

  1. renamed lemmas

    @mckoen
    mckoen committed Jun 22, 2022
    Configuration menu
    Copy the full SHA
    222f853 View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2022

  1. Merge branch 'master' into valuation_maximal

    @mckoen
    mckoen committed Jul 12, 2022
    Configuration menu
    Copy the full SHA
    5f5e971 View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2022

  1. Formatting

    @Vierkantor
    Vierkantor committed Jul 14, 2022
    Configuration menu
    Copy the full SHA
    8971c52 View commit details
    Browse the repository at this point in the history

  2. Show A.nonunits agrees with the maximal ideal of A as an equality… 

    … of subsets of `K`.
    @Vierkantor
    Vierkantor committed Jul 14, 2022
    Configuration menu
    Copy the full SHA
    52fcc37 View commit details
    Browse the repository at this point in the history

  3. Make argument to mem_nonunits_iff implicit because it's on both sid… 

    …es of the `iff`
    @Vierkantor
    Vierkantor committed Jul 14, 2022
    Configuration menu
    Copy the full SHA
    5b2c569 View commit details
    Browse the repository at this point in the history

Commits on Jul 15, 2022

  1. Apply suggestions from code review 

    Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @mckoen @Vierkantor @eric-wieser
    3 people committed Jul 15, 2022
    Configuration menu
    Copy the full SHA
    87ecfba View commit details
    Browse the repository at this point in the history

  2. add K as variable and small golf

    @mckoen
    mckoen committed Jul 15, 2022
    Configuration menu
    Copy the full SHA
    0535212 View commit details
    Browse the repository at this point in the history

  3. correction

    @mckoen
    mckoen committed Jul 15, 2022
    Configuration menu
    Copy the full SHA
    4861ac6 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2022

  1. Update src/ring_theory/valuation/valuation_subring.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @mckoen @jcommelin
    mckoen and jcommelin committed Jul 16, 2022
    Configuration menu
    Copy the full SHA
    167fda5 View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2022

  1. add variable and order embedding

    @mckoen
    mckoen committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    f48a733 View commit details
    Browse the repository at this point in the history