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] - chore(data/pi): add pi.prod and use elsewhere #11877

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - chore(data/pi): add pi.prod and use elsewhere #11877

wants to merge 15 commits into from

Commits on Feb 6, 2022

  1. chore(data/pi): add pi.prod and use elsewhere

    @eric-wieser
    eric-wieser committed Feb 6, 2022
    Configuration menu
    Copy the full SHA
    48c6a22 View commit details
    Browse the repository at this point in the history

  2. lemmas

    @eric-wieser
    eric-wieser committed Feb 6, 2022
    Configuration menu
    Copy the full SHA
    3d78050 View commit details
    Browse the repository at this point in the history

  3. fix

    @eric-wieser
    eric-wieser committed Feb 6, 2022
    Configuration menu
    Copy the full SHA
    d19cfb0 View commit details
    Browse the repository at this point in the history

  4. rfl

    @eric-wieser
    eric-wieser committed Feb 6, 2022
    Configuration menu
    Copy the full SHA
    19938df View commit details
    Browse the repository at this point in the history

  5. fix

    @eric-wieser
    eric-wieser committed Feb 6, 2022
    Configuration menu
    Copy the full SHA
    e240415 View commit details
    Browse the repository at this point in the history

  6. add coe lemma

    @eric-wieser
    eric-wieser committed Feb 6, 2022
    Configuration menu
    Copy the full SHA
    e66213d View commit details
    Browse the repository at this point in the history

Commits on Feb 7, 2022

  1. fix name clash

    @eric-wieser
    eric-wieser committed Feb 7, 2022
    Configuration menu
    Copy the full SHA
    abfa8e1 View commit details
    Browse the repository at this point in the history

  2. fix name clash again

    @eric-wieser
    eric-wieser committed Feb 7, 2022
    Configuration menu
    Copy the full SHA
    747b5c4 View commit details
    Browse the repository at this point in the history

  3. fix

    @eric-wieser
    eric-wieser committed Feb 7, 2022
    Configuration menu
    Copy the full SHA
    0736ef6 View commit details
    Browse the repository at this point in the history

  4. fix

    @eric-wieser
    eric-wieser committed Feb 7, 2022
    Configuration menu
    Copy the full SHA
    48d430e View commit details
    Browse the repository at this point in the history

  5. fix

    @eric-wieser
    eric-wieser committed Feb 7, 2022
    Configuration menu
    Copy the full SHA
    ca34af2 View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2022

  1. fix

    @eric-wieser
    eric-wieser committed Feb 8, 2022
    Configuration menu
    Copy the full SHA
    2cd250e View commit details
    Browse the repository at this point in the history

  2. unrelated golf

    @eric-wieser
    eric-wieser committed Feb 8, 2022
    Configuration menu
    Copy the full SHA
    aff2b18 View commit details
    Browse the repository at this point in the history

  3. Update sensitivity.lean

    @eric-wieser
    eric-wieser committed Feb 8, 2022
    Configuration menu
    Copy the full SHA
    d0bfec3 View commit details
    Browse the repository at this point in the history

  4. fix

    @eric-wieser
    eric-wieser committed Feb 8, 2022
    Configuration menu
    Copy the full SHA
    4a29c61 View commit details
    Browse the repository at this point in the history