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.Basic #5335

Closed
wants to merge 18 commits into from
Closed

[Merged by Bors] - feat: port NumberTheory.Cyclotomic.Basic #5335

wants to merge 18 commits into from

Commits on Jun 21, 2023

  1. feat: port NumberTheory.Cyclotomic.Basic

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

  2. Initial file copy from mathport

    @riccardobrasca
    riccardobrasca committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    444aeca 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 21, 2023
    Configuration menu
    Copy the full SHA
    501b137 View commit details
    Browse the repository at this point in the history

  4. first fixes

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

  5. progress

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

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

    …yclotomic.Basic
    @ChrisHughes24
    ChrisHughes24 committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    c91cdab View commit details
    Browse the repository at this point in the history

  7. fix one proof

    @ChrisHughes24
    ChrisHughes24 committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    937604d View commit details
    Browse the repository at this point in the history

  8. more fixes

    @ChrisHughes24
    ChrisHughes24 committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    efe1b6c View commit details
    Browse the repository at this point in the history

  9. more fixes

    @ChrisHughes24
    ChrisHughes24 committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    59fc03f View commit details
    Browse the repository at this point in the history

  10. small fix

    @ChrisHughes24
    ChrisHughes24 committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    2cbbd8e View commit details
    Browse the repository at this point in the history

  11. trivial fixes

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

  12. this should compile

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

  13. names

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

  14. doc

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

Commits on Jun 22, 2023

  1. Update Mathlib/NumberTheory/Cyclotomic/Basic.lean 

    Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
    @riccardobrasca @urkud
    riccardobrasca and urkud committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    430ec14 View commit details
    Browse the repository at this point in the history

  2. use capital letter

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

  3. add note

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

  4. another note

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