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(number_theory/legendre_symbol/mul_character): alternative implementation #14768

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat(number_theory/legendre_symbol/mul_character): alternative implementation #14768

wants to merge 13 commits into from

Commits on Jun 27, 2022

  1. feat(number_theory/legendre_symbol/mul_character): add new file mul_c… 

    …haracter.lean
    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    b85194f View commit details
    Browse the repository at this point in the history

  2. make suggested changes

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    2d232e6 View commit details
    Browse the repository at this point in the history

  3. variant implemention of multiplicative characters

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    df4420f View commit details
    Browse the repository at this point in the history

  4. fix too long line

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    bc36302 View commit details
    Browse the repository at this point in the history

  5. fix docstrings, add @[simp]s, simplifications

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    b9b695f View commit details
    Browse the repository at this point in the history

  6. add pow_apply'

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    a9b2439 View commit details
    Browse the repository at this point in the history

  7. weaker assumptions, simplifications

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    3f23408 View commit details
    Browse the repository at this point in the history

  8. fix documentation

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    d325397 View commit details
    Browse the repository at this point in the history

  9. make changes suggested by Kevin Buzzard

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    8c746f9 View commit details
    Browse the repository at this point in the history

  10. add comment

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    a4af8b1 View commit details
    Browse the repository at this point in the history

  11. remove decidability instance

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    4f34377 View commit details
    Browse the repository at this point in the history

Commits on Jun 28, 2022

  1. make changes suggested by Vierkantor

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 28, 2022
    Configuration menu
    Copy the full SHA
    36fd93a View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2022

  1. make further suggested changes

    @MichaelStollBayreuth
    MichaelStollBayreuth committed Jun 29, 2022
    Configuration menu
    Copy the full SHA
    1a876ae View commit details
    Browse the repository at this point in the history