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/discrete_valuation_ring): add additive valuation #5094

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(ring_theory/discrete_valuation_ring): add additive valuation #5094

wants to merge 10 commits into from

Commits on Nov 23, 2020

  1. feat(ring_theory/discrete_valuation_ring): add additive valuation

    @kbuzzard
    kbuzzard committed Nov 23, 2020
    Configuration menu
    Copy the full SHA
    d08a2ab View commit details
    Browse the repository at this point in the history

  2. placate linter

    @kbuzzard
    kbuzzard committed Nov 23, 2020
    Configuration menu
    Copy the full SHA
    c4feee7 View commit details
    Browse the repository at this point in the history

  3. saner variable name

    @kbuzzard
    kbuzzard committed Nov 23, 2020
    Configuration menu
    Copy the full SHA
    e737e5c View commit details
    Browse the repository at this point in the history

  4. delete comment

    @kbuzzard
    kbuzzard committed Nov 23, 2020
    Configuration menu
    Copy the full SHA
    99017e0 View commit details
    Browse the repository at this point in the history

  5. clarify comment

    @kbuzzard
    kbuzzard committed Nov 23, 2020
    Configuration menu
    Copy the full SHA
    19e12f2 View commit details
    Browse the repository at this point in the history

Commits on Nov 25, 2020

  1. golf proof

    @kbuzzard
    kbuzzard committed Nov 25, 2020
    Configuration menu
    Copy the full SHA
    9a292e7 View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2020

  1. Update src/ring_theory/discrete_valuation_ring.lean 

    Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
    @kbuzzard @robertylewis
    kbuzzard and robertylewis committed Dec 4, 2020
    Configuration menu
    Copy the full SHA
    0f2ab70 View commit details
    Browse the repository at this point in the history

  2. Update src/ring_theory/discrete_valuation_ring.lean 

    Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
    @kbuzzard @Vierkantor
    kbuzzard and Vierkantor committed Dec 4, 2020
    Configuration menu
    Copy the full SHA
    65cfe11 View commit details
    Browse the repository at this point in the history

  3. Update src/ring_theory/discrete_valuation_ring.lean 

    Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
    @kbuzzard @robertylewis
    kbuzzard and robertylewis committed Dec 4, 2020
    Configuration menu
    Copy the full SHA
    c0f4026 View commit details
    Browse the repository at this point in the history

  4. fix 101 character line

    @kbuzzard
    kbuzzard committed Dec 4, 2020
    Configuration menu
    Copy the full SHA
    c0dd4aa View commit details
    Browse the repository at this point in the history