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: changeLevel for Dirichlet characters #7263

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: changeLevel for Dirichlet characters #7263

wants to merge 13 commits into from

Commits on Sep 19, 2023

  1. feat: change_level for Dirichlet characters

    @mo271
    mo271 committed Sep 19, 2023
    Configuration menu
    Copy the full SHA
    6394171 View commit details
    Browse the repository at this point in the history

  2. add author

    @mo271
    mo271 committed Sep 19, 2023
    Configuration menu
    Copy the full SHA
    2a9e5ad View commit details
    Browse the repository at this point in the history

  3. add author

    @mo271
    mo271 committed Sep 19, 2023
    Configuration menu
    Copy the full SHA
    e419f62 View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2023

  1. more lemmas

    @mo271
    mo271 committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    e993783 View commit details
    Browse the repository at this point in the history

  2. change_level -> changeLevel

    @mo271
    mo271 committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    d27ac21 View commit details
    Browse the repository at this point in the history

  3. more ZMod.unitsMap

    @mo271
    mo271 committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    4a29859 View commit details
    Browse the repository at this point in the history

  4. less ZMod

    @mo271
    mo271 committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    9f1237e View commit details
    Browse the repository at this point in the history

  5. even less Zmod

    @mo271
    mo271 committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    06b3f4e View commit details
    Browse the repository at this point in the history

  6. add unitsMap_comp

    @mo271
    mo271 committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    7db676c View commit details
    Browse the repository at this point in the history

  7. review comments

    @mo271
    mo271 committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    59c4b2e View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/NumberTheory/DirichletCharacter/Basic.lean 

    Co-authored-by: Alex J Best <alex.j.best@gmail.com>
    @mo271 @alexjbest
    mo271 and alexjbest committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    783d8e0 View commit details
    Browse the repository at this point in the history

  9. Update Mathlib/Data/ZMod/Units.lean 

    Co-authored-by: Alex J Best <alex.j.best@gmail.com>
    @mo271 @alexjbest
    mo271 and alexjbest committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    92aaa9f View commit details
    Browse the repository at this point in the history

  10. fit on one line

    @mo271
    mo271 committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    6cfd285 View commit details
    Browse the repository at this point in the history