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 principal unit group of valuation subring and provide basic API #14742

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat(ring_theory/valuation/valuation_subring): define principal unit group of valuation subring and provide basic API #14742

wants to merge 28 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

  3. principal units

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

  4. lemmas

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

Commits on Jun 14, 2022

  1. shorter

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

  2. even shorter

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

Commits on Jun 21, 2022

  1. add a couple of small sorries

    @adamtopaz
    adamtopaz committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    b2c52cd View commit details
    Browse the repository at this point in the history

Commits on Jun 25, 2022

  1. wip lemmas

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

Commits on Jun 28, 2022

  1. to be cleaned up

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

Commits on Jun 29, 2022

  1. polished

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

Commits on Jul 10, 2022

  1. small simps

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

Commits on Jul 24, 2022

  1. add a few lemmas

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

Commits on Jul 26, 2022

  1. sloppy merge

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

  2. move lines

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

Commits on Jul 27, 2022

  1. formatting

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

Commits on Jul 29, 2022

  1. golf injectivity

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

Commits on Jul 31, 2022

  1. golf

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

Commits on Aug 6, 2022

  1. add lemmas

    @mckoen
    mckoen committed Aug 6, 2022
    Configuration menu
    Copy the full SHA
    0c82af5 View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2022

  1. add doc string and lemmas

    @mckoen
    mckoen committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    6bcf5cd View commit details
    Browse the repository at this point in the history

  2. remove parentheses

    @mckoen
    mckoen committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    3e61008 View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2022

  1. add lemmas

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

  2. fix

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

  3. fix

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

  4. last fix

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