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: port Data.Real.Sign #1618

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat: port Data.Real.Sign #1618

wants to merge 6 commits into from

Commits on Jan 17, 2023

  1. feat: port Data.Real.Sign

    @qawbecrdtey
    qawbecrdtey committed Jan 17, 2023
    Configuration menu
    Copy the full SHA
    b959f24 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @qawbecrdtey
    qawbecrdtey committed Jan 17, 2023
    Configuration menu
    Copy the full SHA
    0f71d17 View commit details
    Browse the repository at this point in the history

  3. Mathbin -> Mathlib; add import to Mathlib.lean

    @qawbecrdtey
    qawbecrdtey committed Jan 17, 2023
    Configuration menu
    Copy the full SHA
    6d1dc4a View commit details
    Browse the repository at this point in the history

  4. Initial commit

    @qawbecrdtey
    qawbecrdtey committed Jan 17, 2023
    Configuration menu
    Copy the full SHA
    fb532cc View commit details
    Browse the repository at this point in the history

  5. Fix int to Int

    @qawbecrdtey
    qawbecrdtey committed Jan 17, 2023
    Configuration menu
    Copy the full SHA
    d8862c6 View commit details
    Browse the repository at this point in the history

  6. Fix misplacement of by

    @qawbecrdtey
    qawbecrdtey committed Jan 17, 2023
    Configuration menu
    Copy the full SHA
    62193d2 View commit details
    Browse the repository at this point in the history