[Merged by Bors] - feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean #15684

MichaelStollBayreuth · 2022-07-26T03:00:29Z

This adds a file to the number_theory/legendre_symbol directory. It defines the Gauss sum of a multiplicative and an additive character on a finite commutative ring with values in another commutative ring and proves some statements about them. This will lead to a new proof of Quadratic Reciprocity (including the second supplementary law).

For comments/discussion, use this Zulip topic.

src/number_theory/legendre_symbol/gauss_sum.lean

src/number_theory/legendre_symbol/add_character.lean

src/algebra/big_operators/fin.lean

src/number_theory/legendre_symbol/add_character.lean

src/number_theory/legendre_symbol/gauss_sum.lean

alreadydone

Here are just some stylistic comments; I plan to take a look at the proofs later today.

src/number_theory/legendre_symbol/add_character.lean

src/number_theory/legendre_symbol/gauss_sum.lean

src/number_theory/legendre_symbol/add_character.lean

src/number_theory/legendre_symbol/gauss_sum.lean

alreadydone · 2022-07-30T06:59:00Z

Golfed some proofs; will continue tomorrow! https://github.com/leanprover-community/mathlib/compare/gauss_sum...alreadydone:mathlib:gauss_sum?expand=1

alreadydone · 2022-07-31T22:36:29Z

Alright I've finished golfing the last proof and now it takes < 7 seconds on my machine. An observation is that using exact_mod_cast to prove ((8 : ℕ) : F) = (8 : F) almost takes two more seconds than norm_num. Another thing I did is extracting the lemma algebra.ring_char_eq. I'm regretful that I'm unable to golf this simp only; it's almost defeq but the numerals differ by an int_cast.
Please let me know if you think some changes are not good; otherwise feel free to merge.

MichaelStollBayreuth · 2022-08-01T01:34:18Z

Thanks! I had noticed that the long last proof took a while.
I have moved the second helper lemma to add_character.lean and made it public (and renamed it).
I've left the first one private for now.

alreadydone

Thanks!

jcommelin

This is now converging rapidly. Thanks @MichaelStollBayreuth for the PR.

Thanks @alreadydone for the review.

src/number_theory/legendre_symbol/gauss_sum.lean

jcommelin

Mini-minor comments. You can merge this after addressing them.

bors d+

src/number_theory/legendre_symbol/gauss_sum.lean

bors · 2022-08-02T06:57:34Z

✌️ MichaelStollBayreuth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

MichaelStollBayreuth · 2022-08-02T15:16:06Z

bors r+

#15684) This adds a file to the number_theory/legendre_symbol directory. It defines the Gauss sum of a multiplicative and an additive character on a finite commutative ring with values in another commutative ring and proves some statements about them. This will lead to a new proof of Quadratic Reciprocity (including the second supplementary law). For comments/discussion, use this [Zulip topic](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Gauss.20sums/near/290844370).

bors · 2022-08-02T17:04:27Z

Pull request successfully merged into master.

Build succeeded:

#15684) This adds a file to the number_theory/legendre_symbol directory. It defines the Gauss sum of a multiplicative and an additive character on a finite commutative ring with values in another commutative ring and proves some statements about them. This will lead to a new proof of Quadratic Reciprocity (including the second supplementary law). For comments/discussion, use this [Zulip topic](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Gauss.20sums/near/290844370).

feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean

ec3109e

MichaelStollBayreuth added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jul 26, 2022

jcommelin reviewed Jul 26, 2022

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 26, 2022

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 26, 2022

MichaelStollBayreuth added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Jul 26, 2022

make suggested changes

23cb675

MichaelStollBayreuth added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 26, 2022

group structure on add_char

42c33d3

jcommelin reviewed Jul 27, 2022

View reviewed changes

src/number_theory/legendre_symbol/gauss_sum.lean Outdated Show resolved Hide resolved

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 27, 2022

eric-wieser reviewed Jul 27, 2022

View reviewed changes

src/number_theory/legendre_symbol/add_character.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth added 3 commits July 27, 2022 23:17

use ψ ^ p in place of mul_shift ψ p

f42b93f

add expansion of short products/sums, make add_char semireducible

39bf3e2

fix docstring, remove commented out line

20c73a1

alreadydone reviewed Jul 28, 2022

View reviewed changes

src/algebra/big_operators/fin.lean Outdated Show resolved Hide resolved

alreadydone reviewed Jul 28, 2022

View reviewed changes

src/number_theory/legendre_symbol/add_character.lean Outdated Show resolved Hide resolved

more efficient proofs of fin.prod_univ_..., give name to instance

6e52733

MichaelStollBayreuth added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 28, 2022

eric-wieser reviewed Jul 28, 2022

View reviewed changes

src/number_theory/legendre_symbol/add_character.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 28, 2022

View reviewed changes

src/number_theory/legendre_symbol/add_character.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 28, 2022

View reviewed changes

src/number_theory/legendre_symbol/gauss_sum.lean Outdated Show resolved Hide resolved

add info to doc string, simplification in add_char.has_inv

c85a766

alreadydone reviewed Jul 29, 2022

View reviewed changes

stylistic changes, change statement of gauss_sum_mul_aux₂

17b4773

MichaelStollBayreuth added 4 commits August 1, 2022 03:12

golf proofs as suggested

a343d1e

add lemma algebra.ring_char_eq

d6ce2fd

move gauss_sum_mul_aux₂ to add_character.lean

16bb5ca

fix comment, add question

dff21bc

alreadydone approved these changes Aug 1, 2022

View reviewed changes

jcommelin reviewed Aug 1, 2022

View reviewed changes

src/number_theory/legendre_symbol/gauss_sum.lean Outdated Show resolved Hide resolved

src/number_theory/legendre_symbol/gauss_sum.lean Outdated Show resolved Hide resolved

src/number_theory/legendre_symbol/gauss_sum.lean Outdated Show resolved Hide resolved

move section start, add namespace to two names

2d09642

jcommelin reviewed Aug 2, 2022

View reviewed changes

src/number_theory/legendre_symbol/gauss_sum.lean Outdated Show resolved Hide resolved

src/number_theory/legendre_symbol/gauss_sum.lean Outdated Show resolved Hide resolved

src/number_theory/legendre_symbol/gauss_sum.lean Outdated Show resolved Hide resolved

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Aug 2, 2022

make changes as suggested

49b928f

bors bot changed the title ~~feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean~~ [Merged by Bors] - feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean Aug 2, 2022

bors bot closed this Aug 2, 2022

bors bot deleted the gauss_sum branch August 2, 2022 17:04

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean #15684

[Merged by Bors] - feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean #15684

MichaelStollBayreuth commented Jul 26, 2022 •

edited

Loading

alreadydone left a comment

alreadydone commented Jul 30, 2022

alreadydone commented Jul 31, 2022 •

edited

Loading

MichaelStollBayreuth commented Aug 1, 2022

alreadydone left a comment

jcommelin left a comment

jcommelin left a comment

bors bot commented Aug 2, 2022

MichaelStollBayreuth commented Aug 2, 2022

bors bot commented Aug 2, 2022

[Merged by Bors] - feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean #15684

[Merged by Bors] - feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean #15684

Conversation

MichaelStollBayreuth commented Jul 26, 2022 • edited Loading

alreadydone left a comment

Choose a reason for hiding this comment

alreadydone commented Jul 30, 2022

alreadydone commented Jul 31, 2022 • edited Loading

MichaelStollBayreuth commented Aug 1, 2022

alreadydone left a comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Aug 2, 2022

MichaelStollBayreuth commented Aug 2, 2022

bors bot commented Aug 2, 2022

MichaelStollBayreuth commented Jul 26, 2022 •

edited

Loading

alreadydone commented Jul 31, 2022 •

edited

Loading