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

feat: add a FloorSemiring instance to NNRat #13548

Open
wants to merge 22 commits into
base: master
Choose a base branch
from
Open

feat: add a FloorSemiring instance to NNRat #13548

wants to merge 22 commits into from
+159 −3

Commits on Jun 5, 2024

  1. feat: add lemmas for NNRat

    @eric-wieser
    eric-wieser committed Jun 5, 2024
    Configuration menu
    Copy the full SHA
    46361cf View commit details
    Browse the repository at this point in the history

Commits on Jun 6, 2024

  1. more

    @eric-wieser
    eric-wieser committed Jun 6, 2024
    Configuration menu
    Copy the full SHA
    987cddc View commit details
    Browse the repository at this point in the history

  2. whitespace

    @eric-wieser
    eric-wieser committed Jun 6, 2024
    Configuration menu
    Copy the full SHA
    1d468be View commit details
    Browse the repository at this point in the history

  3. feat: add a FloorSemiring instance to nnrat

    @eric-wieser
    eric-wieser committed Jun 6, 2024
    Configuration menu
    Copy the full SHA
    d00d944 View commit details
    Browse the repository at this point in the history

  4. fix

    @eric-wieser
    eric-wieser committed Jun 6, 2024
    Configuration menu
    Copy the full SHA
    e4a084e View commit details
    Browse the repository at this point in the history

  5. whitespace

    @eric-wieser
    eric-wieser committed Jun 6, 2024
    Configuration menu
    Copy the full SHA
    41f1de7 View commit details
    Browse the repository at this point in the history

Commits on Jun 9, 2024

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/nnrat-f… 

    …loor
    @eric-wieser
    eric-wieser committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    7e41bc7 View commit details
    Browse the repository at this point in the history

  2. working

    @eric-wieser
    eric-wieser committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    422a5d5 View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2024

  1. Merge branch 'master' into eric-wieser/nnrat-floor

    @eric-wieser
    eric-wieser authored Jul 22, 2024
    Configuration menu
    Copy the full SHA
    42db170 View commit details
    Browse the repository at this point in the history

  2. Update Floor.lean

    @eric-wieser
    eric-wieser authored Jul 22, 2024
    Configuration menu
    Copy the full SHA
    8c3eb6e View commit details
    Browse the repository at this point in the history

  3. add import

    @eric-wieser
    eric-wieser committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    900b41f View commit details
    Browse the repository at this point in the history

  4. add lemmas

    @eric-wieser
    eric-wieser committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    8e1768d View commit details
    Browse the repository at this point in the history

  5. more silly lemmas

    @eric-wieser
    eric-wieser committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    fbed638 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2024

  1. shake

    @eric-wieser
    eric-wieser committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    0c0206f View commit details
    Browse the repository at this point in the history

Commits on Aug 5, 2024

  1. grammar fix

    @eric-wieser
    eric-wieser committed Aug 5, 2024
    Configuration menu
    Copy the full SHA
    97859f6 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into eric-wieser/nnrat-f… 

    …loor
    @eric-wieser
    eric-wieser committed Aug 5, 2024
    Configuration menu
    Copy the full SHA
    0459227 View commit details
    Browse the repository at this point in the history

Commits on Aug 18, 2024

  1. more lemmas

    @eric-wieser
    eric-wieser committed Aug 18, 2024
    Configuration menu
    Copy the full SHA
    a5f49e8 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into eric-wieser/nnrat-f… 

    …loor
    @eric-wieser
    eric-wieser committed Aug 18, 2024
    Configuration menu
    Copy the full SHA
    a62409e View commit details
    Browse the repository at this point in the history

  3. sorry-free

    @eric-wieser
    eric-wieser committed Aug 18, 2024
    Configuration menu
    Copy the full SHA
    b7d6be9 View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2024

  1. fix deprecation

    @eric-wieser
    eric-wieser committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    e30bc10 View commit details
    Browse the repository at this point in the history

Commits on Aug 31, 2024

  1. add @[simp]

    @eric-wieser
    eric-wieser committed Aug 31, 2024
    Configuration menu
    Copy the full SHA
    eaa6533 View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2024

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/nnrat-f… 

    …loor
    @eric-wieser
    eric-wieser committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    6d6f59b View commit details
    Browse the repository at this point in the history