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 NumberTheory.Cyclotomic.Rat #5417

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat: port NumberTheory.Cyclotomic.Rat #5417

wants to merge 15 commits into from

Commits on Jun 23, 2023

  1. feat: port NumberTheory.Cyclotomic.Rat

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    80ac9b4 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    bfeeebf View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    576c1be View commit details
    Browse the repository at this point in the history

  4. good progress

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    72f887c View commit details
    Browse the repository at this point in the history

  5. chore: use _root_. as in mathlib3

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    c5a18e4 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'RB/fix_namespace' into port/NumberTheory.Cyclotomic.Rat

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    d6f714b View commit details
    Browse the repository at this point in the history

  7. better

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    8d7169b View commit details
    Browse the repository at this point in the history

  8. Merge remote-tracking branch 'origin/master' into port/NumberTheory.C… 

    …yclotomic.Rat
    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    86fd404 View commit details
    Browse the repository at this point in the history

  9. better

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    bd78f26 View commit details
    Browse the repository at this point in the history

  10. progress

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    97813e7 View commit details
    Browse the repository at this point in the history

  11. better statements

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    3d45a19 View commit details
    Browse the repository at this point in the history

  12. Merge remote-tracking branch 'origin/master' into RB/PowerBasis'

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    5406f17 View commit details
    Browse the repository at this point in the history

  13. Merge branch 'RB/PowerBasis'' into port/NumberTheory.Cyclotomic.Rat

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    cc7e919 View commit details
    Browse the repository at this point in the history

  14. ths should compile

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    b154f5e View commit details
    Browse the repository at this point in the history

  15. names

    @riccardobrasca
    riccardobrasca committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    6e638c5 View commit details
    Browse the repository at this point in the history