[Merged by Bors] - feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)| #12595

ericrbg · 2022-03-11T17:18:20Z

Originally from the Wedderburn PR, but generalized to include an exponent.

Co-authored-by: Alex J. Best alex.j.best@gmail.com

depends on: [Merged by Bors] - feat(analysis/convex/strict_convex_space): Ray characterization of ∥x - y∥ #13293
depends on: [Merged by Bors] - feat(algebra/*/basic): add trivial lemmas #13416
depends on: [Merged by Bors] - feat(complex/roots_of_unity): extensionality #13431
depends on: [Merged by Bors] - feat(complex/arg): arg_eq_zero_iff #13432
depends on: [Merged by Bors] - feat(algebra/big_operators/basic): mk0_prod #13582
depends on: [Merged by Bors] - feat(polynomial/cyclotomic): eval_apply #13586
depends on: [Merged by Bors] - chore(ring_theory/roots_of_unity): primitive roots are not zero #13587
depends on: [Merged by Bors] - feat(data/nat/totient): totient equals one iff #13688

this is a real large yak...

Co-authored-by: Johan Commelin <johan@commelin.net>

riccardobrasca · 2022-03-11T17:24:47Z

I don't remember the details, but I have the impression that with this result you can golf a little bit the proof of nat.exists_prime_ge_modeq_one (at the beginning we need that eval _ cyclotomic is bigger then 1 or something like that).

Also, no problem the the requested review, but can you erase your comment from the PR description? I think that description ends up in the "official" Zulip stream.

ericrbg · 2022-03-11T17:26:06Z

ah, I'll have a look.

and no, the "top" bit I think is what ends up on the PR description, as far as I understand the bit below the line is just for discussion whilst writing the PR

riccardobrasca · 2022-03-11T17:26:54Z

ah, I'll have a look.

and no, the "top" bit I think is what ends up on the PR description, as far as I understand the bit below the line is just for discussion whilst writing the PR

That's very possible.

riccardobrasca · 2022-03-11T17:30:28Z

src/ring_theory/polynomial/cyclotomic/eval.lean

@@ -160,4 +160,52 @@ begin
    exact nat.pow_right_injective hp.two_le hxy }
 end

+lemma sub_one_lt_nat_abs_cyclotomic_eval (n : ℕ) (q : ℕ) (hn' : 1 < n) (hq' : q ≠ 1) :


Can you add some comments explaining the proof? It doesn't look trivial

riccardobrasca · 2022-03-11T17:33:39Z

src/ring_theory/polynomial/cyclotomic/eval.lean

+             ring_hom.eq_int_cast, eval_sub],
+  rw [←finset.prod_sdiff (finset.singleton_subset_iff.mpr $ (mem_primitive_roots hn).mpr hζ),
+      finset.prod_singleton, ←one_mul (↑(q - 1) : nnreal)],
+  have aux : 1 ≤ ∏ (x : ℂ) in primitive_roots n ℂ \ {ζ}, ∥↑q - x∥₊,


This can be extracted as a separate lemma I think.

alexjbest · 2022-03-13T02:00:51Z

I think there is a potentially more useful stronger version of this result, where we instead get (q - 1) ^ totient n < (cyclotomic n ℝ).eval q (for any real > 1). The proof is somewhat the same so I've been modifying whats here to give that result instead as it seems nice to get the best possible version. (there is an upper bound version too)

I know that this stronger version is used in a proof of Zsigmondy's theorem for instance.

Would you mind waiting a day or two until thats done, and then I'll push it here?

ericrbg · 2022-03-13T02:30:02Z

Sure, feel free to push and I'll fix it up then. I was busy this weekend anyways so it all works out ^^

alexjbest · 2022-03-14T17:23:30Z

Ok I've pushed where I'm up to, its sorry free, but a bit of a monster proof. I really had to fight super hard to apply prod_lt_prod' as it needs an ordered cancel monoid, so I had to move everything to positive reals (by taking the units of nnreal). It makes me wonder if we need some other versions of that theorem that are easier to apply, but I'm not sure how.

Anyone should feel free to fix up my bad work, I'll keep chipping away at it too. I just didn't want to hold the branch hostage any longer ;).

Note that I added the statement for the upper bound too, I can't see a sneaky way to reuse the same proof, or use one to prove the other (note the upper bound has a stronger condition on n). So maybe we can just copy paste when the proof is minimized a bit.

src/ring_theory/polynomial/cyclotomic/eval.lean

leanprover-community-bot-assistant · 2022-04-25T20:05:05Z

This PR/issue depends on:

~~[Merged by Bors] - feat(analysis/convex/strict_convex_space): Ray characterization of ∥x - y∥ #13293~~
~~[Merged by Bors] - feat(algebra/*/basic): add trivial lemmas #13416~~
~~[Merged by Bors] - feat(complex/roots_of_unity): extensionality #13431~~
~~[Merged by Bors] - feat(complex/arg): arg_eq_zero_iff #13432~~
~~[Merged by Bors] - feat(algebra/big_operators/basic): mk0_prod #13582~~
~~[Merged by Bors] - feat(polynomial/cyclotomic): eval_apply #13586~~
~~[Merged by Bors] - chore(ring_theory/roots_of_unity): primitive roots are not zero #13587~~
~~[Merged by Bors] - feat(data/nat/totient): totient equals one iff #13688~~
By Dependent Issues (🤖). Happy coding!

riccardobrasca

Can you have a quick look at the proof of nat.exists_prime_ge_modeq_one? It can maybe be golfed using this (and one variable should be made implicit)

src/ring_theory/polynomial/cyclotomic/eval.lean

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

ericrbg · 2022-04-28T18:00:51Z

If it can, it won't be too huge of a golf - because these theorems require 1 < k (for k being the number of the cyclotomic poly) but yours needs 0 < n. (it is of course a ≤ for all 0 < k, should I add this version too?)

riccardobrasca · 2022-04-28T18:05:18Z

That's not so important, don't worry.

riccardobrasca · 2022-04-28T18:06:34Z

Let's just get this merged, thanks!

bors d+

bors · 2022-04-28T18:06:35Z

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

ericrbg · 2022-04-28T19:46:57Z

bors r+

Originally from the Wedderburn PR, but generalized to include an exponent. Co-authored-by: Alex J. Best <alex.j.best@gmail.com> Co-authored-by: Alex J. Best <alex.j.best@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Alex J Best <alex.j.best@gmail.com>

bors · 2022-04-28T20:22:49Z

Pull request successfully merged into master.

Build succeeded:

As suggested in the reviews of #12595 we try to golf the proof using the bound proved there. This doesn't end up being as much of a golf as hoped due to annoying edge cases, but seems conceptually simpler.

feat(cyclotomic/eval): q - 1 < |ϕₙ(q)|

5afc0fd

Co-authored-by: Johan Commelin <johan@commelin.net>

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

ericrbg requested review from jcommelin and riccardobrasca March 11, 2022 17:18

ericrbg mentioned this pull request Mar 11, 2022

feat(ring_theory): Wedderburn's little theorem (finite domains are fields) #9856

Open

9 tasks

riccardobrasca reviewed Mar 11, 2022

View reviewed changes

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

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 Mar 12, 2022

generalize

238d15e

alexjbest changed the title ~~feat(cyclotomic/eval): q - 1 < |ϕₙ(q)|~~ feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)| Mar 14, 2022

alexjbest and others added 6 commits March 14, 2022 18:33

original

1e1f9f4

ew

527c1a9

golf

c70df62

golf a bit

ab1157a

minigolf

de71ec1

extract a lemma

1584a0c

riccardobrasca reviewed Mar 15, 2022

View reviewed changes

src/ring_theory/polynomial/cyclotomic/eval.lean Show resolved Hide resolved

some random golfs

1b8958d

ericrbg added the WIP Work in progress label Mar 15, 2022

alexjbest reviewed Mar 15, 2022

View reviewed changes

src/ring_theory/polynomial/cyclotomic/eval.lean Outdated Show resolved Hide resolved

alexjbest and others added 2 commits March 15, 2022 16:46

Update src/ring_theory/polynomial/cyclotomic/eval.lean

73a0811

some more stuff, let's wait for convexity now

1e2721b

leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 25, 2022

ericrbg added 2 commits April 25, 2022 21:43

Merge remote-tracking branch 'origin/master' into lt_eval_cyclotomic

50c2e67

maybe ready?

90da978

ericrbg 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. and removed WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes labels Apr 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 Apr 26, 2022

leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 26, 2022

merge

ec7d91a

leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 27, 2022

Merge remote-tracking branch 'origin/master' into lt_eval_cyclotomic

a3bccda

riccardobrasca approved these changes Apr 27, 2022

View reviewed changes

src/ring_theory/polynomial/cyclotomic/eval.lean Outdated Show resolved Hide resolved

src/ring_theory/polynomial/cyclotomic/eval.lean Outdated Show resolved Hide resolved

src/ring_theory/polynomial/cyclotomic/eval.lean Outdated Show resolved Hide resolved

ericrbg and others added 2 commits April 28, 2022 13:47

implicitify

60a3cbd

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

tidy

6533557

github-actions bot 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 Apr 28, 2022

bors bot changed the title ~~feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)|~~ [Merged by Bors] - feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)| Apr 28, 2022

bors bot closed this Apr 28, 2022

bors bot deleted the lt_eval_cyclotomic branch April 28, 2022 20:22

alexjbest mentioned this pull request Apr 29, 2022

[Merged by Bors] - feat(number_theory/primes_congruent_one): attempt to golf #13787

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)| #12595

[Merged by Bors] - feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)| #12595

ericrbg commented Mar 11, 2022 •

edited by github-actions bot

riccardobrasca commented Mar 11, 2022

ericrbg commented Mar 11, 2022

riccardobrasca commented Mar 11, 2022

riccardobrasca Mar 11, 2022

riccardobrasca Mar 11, 2022

alexjbest commented Mar 13, 2022 •

edited

ericrbg commented Mar 13, 2022

alexjbest commented Mar 14, 2022

leanprover-community-bot-assistant commented Apr 25, 2022

riccardobrasca left a comment

ericrbg commented Apr 28, 2022 •

edited

riccardobrasca commented Apr 28, 2022

riccardobrasca commented Apr 28, 2022

bors bot commented Apr 28, 2022

ericrbg commented Apr 28, 2022

bors bot commented Apr 28, 2022

[Merged by Bors] - feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)| #12595

[Merged by Bors] - feat(cyclotomic/eval): (q - 1) ^ totient n < |ϕₙ(q)| #12595

Conversation

ericrbg commented Mar 11, 2022 • edited by github-actions bot

riccardobrasca commented Mar 11, 2022

ericrbg commented Mar 11, 2022

riccardobrasca commented Mar 11, 2022

riccardobrasca Mar 11, 2022

Choose a reason for hiding this comment

riccardobrasca Mar 11, 2022

Choose a reason for hiding this comment

alexjbest commented Mar 13, 2022 • edited

ericrbg commented Mar 13, 2022

alexjbest commented Mar 14, 2022

leanprover-community-bot-assistant commented Apr 25, 2022

riccardobrasca left a comment

Choose a reason for hiding this comment

ericrbg commented Apr 28, 2022 • edited

riccardobrasca commented Apr 28, 2022

riccardobrasca commented Apr 28, 2022

bors bot commented Apr 28, 2022

ericrbg commented Apr 28, 2022

bors bot commented Apr 28, 2022

ericrbg commented Mar 11, 2022 •

edited by github-actions bot

alexjbest commented Mar 13, 2022 •

edited

ericrbg commented Apr 28, 2022 •

edited