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.
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
[Merged by Bors] - feat(number_theory/legendre_symbol/mul_character): alternative implementation #14768
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks great to me -- thanks very much Michael! Dirichlet characters, a special case of this, will be a very welcome addition to mathlib.
cad5c63
to
4f34377
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Unfortunately I couldn't finish the review today, the shops are closing soon.
These may look like a lot of suggestions, but most are relatively minor and repeated a few times.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you for your work! It looks good to me with these changes.
bors d+
✌️ MichaelStollBayreuth can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…entation (#14768) This is an alternative version of `number_theory/legendre_symbol/mul_character.lean`. It defines `mul_character R R'` as a `monoid_hom` that sends non-units to zero. This allows to define a `comm_group` structure on `mul_character R R'`. There is an alternative implementation in #14716 ([side by side comparison](legendre_symbol_mul_char...variant)). See the [discussion on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implementation.20of.20multiplicative.20characters).
Pull request successfully merged into master. Build succeeded: |
…as `mul_char`s (#15418) This is a follow-up to #14768; it defines quadratic characters (and also the characters on `zmod 4` and `zmod 8`) to be of type `mul_char F int` (where `F` is a finite field). Some content of `number_theory/legendre_symbol/quadratic_char` is moved within the file; one proof is replaced by directly using the corresponding more general result. See here on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implementation.20of.20multiplicative.20characters/near/289635166).
…as `mul_char`s (#15418) This is a follow-up to #14768; it defines quadratic characters (and also the characters on `zmod 4` and `zmod 8`) to be of type `mul_char F int` (where `F` is a finite field). Some content of `number_theory/legendre_symbol/quadratic_char` is moved within the file; one proof is replaced by directly using the corresponding more general result. See here on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implementation.20of.20multiplicative.20characters/near/289635166).
…as `mul_char`s (#15418) This is a follow-up to #14768; it defines quadratic characters (and also the characters on `zmod 4` and `zmod 8`) to be of type `mul_char F int` (where `F` is a finite field). Some content of `number_theory/legendre_symbol/quadratic_char` is moved within the file; one proof is replaced by directly using the corresponding more general result. See here on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implementation.20of.20multiplicative.20characters/near/289635166).
…as `mul_char`s (#15418) This is a follow-up to #14768; it defines quadratic characters (and also the characters on `zmod 4` and `zmod 8`) to be of type `mul_char F int` (where `F` is a finite field). Some content of `number_theory/legendre_symbol/quadratic_char` is moved within the file; one proof is replaced by directly using the corresponding more general result. See here on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implementation.20of.20multiplicative.20characters/near/289635166).
This is an alternative version of
number_theory/legendre_symbol/mul_character.lean
.It defines
mul_character R R'
as amonoid_hom
that sends non-units to zero.This allows to define a
comm_group
structure onmul_character R R'
.There is an alternative implementation in #14716 (side by side comparison).
See the discussion on Zulip.