[Merged by Bors] - feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g #10767

ericrbg · 2021-12-13T19:24:45Z

Precursor to #10692.

depends on: [Merged by Bors] - feat(data/nat/prime): dvd_of_factors_subperm #10764
depends on: [Merged by Bors] - feat(number_theory/padics/padic_norm): lemmas #10765
depends on: [Merged by Bors] - feat(group_theory/order_of_element): additivize #10766

~~My brain is too frazzled right now, but here's a proof with one sorry of the same fact without the fintype requirement (for fintype, order_of_pos immediately gets us back to this version).~~

ericrbg · 2021-12-13T21:56:47Z

I finished that one sorry!

github-actions · 2021-12-14T11:26:06Z

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

Julian-Kuelshammer · 2021-12-14T15:58:47Z

src/group_theory/exponent.lean

+end
+
+@[to_additive]
+lemma exponent_eq_zero_of_order_zero {g : G} (hg : order_of g = 0) : exponent G = 0 :=


Should the name rather be exponent_eq_zero_of_order_of_eq_zero?

I feel like in the rest of the file, order has been used interchangably with order_of; I can change it but I prefer snappier names (at least as much as possible within the naming conventions)

Should we rename order_of to order? And update all the names? (Not in this PR, of course.)

I'd be in favour of that!

src/group_theory/exponent.lean

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

jcommelin · 2021-12-18T17:50:40Z

src/group_theory/exponent.lean

+
+variable [cancel_comm_monoid G]
+
+@[to_additive] lemma exponent_eq_Sup_order_of (h : ∀ g : G, 0 < order_of g) :


Do you see any way to split/golf this proof? Intuitively, I think it looks a lot longer than I would expect a proof of this result to be. But I haven't loaded it into VScode yet.

my only thoughts are that the first half could maybe be made into a private lemma, and the second half could be turned into a calc; but I'm fairly bad at calc. If you want me to turn the first edge case into a separate lemma, though, I can do that!

the order arguments were a lot more finicky here than I expected; I wish I could just say "if g has order not dividing t (which maximises the group's order), then g*t clearly has larger order"; but this statement requires a fair bit more care than I thought

jcommelin · 2021-12-22T21:26:04Z

I've extracted the first half of the big proof into a lemma. Because I think it is a generally useful statement.
The other half of the big proof still feels slow to me.

ericrbg · 2021-12-22T22:25:44Z

thanks! it does look very useful, now that you extracted it. I think I sped up the proof a lot, the main culprit was ac_refl, but there was misc other things too. I hope we can get tactics that ignore associativity performantly in Lean4!

ericrbg · 2021-12-22T22:27:18Z

src/group_theory/exponent.lean

+      pow_add, pow_add, pow_one, ←mul_assoc, ←mul_assoc, nat.div_mul_cancel, mul_assoc,
+      lt_mul_iff_one_lt_right $ h t, ←pow_succ'],
+  exact one_lt_pow hp.1.one_lt a.succ_ne_zero,
+  exact hpk


I'm really confused as to why, but if you put this hpk where it belongs in the monster rw (after nat.div_mul_cancel) then the rewrite fails completely. ¯\_(ツ)_/¯

urkud · 2021-12-23T15:23:58Z

src/group_theory/exponent.lean

+variable [cancel_comm_monoid G]
+
+@[to_additive] lemma exponent_eq_Sup_order_of (h : ∀ g : G, 0 < order_of g) :
+  exponent G = Sup (set.range (order_of : G → ℕ)) :=


We usually use supr for Sup (set.range _). It's definitionally the same but comes with nice notation and lemmas.

Ooh, I didn't know about this. Is there an alternative for finset as well, or should I just leave that as max'?

I just ended up just rw supr at the start; it seems to me that for proving things about it the Sup API is a bit better. But the csupr induction seemed cool; if I was rewriting the proof, I'd probably use that.

jcommelin

Thanks 🎉

bors merge

Precursor to #10692. Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>

bors · 2021-12-23T20:58:09Z

Pull request successfully merged into master.

Build succeeded:

ericrbg added 9 commits December 13, 2021 17:45

feat(data/nat/prime): dvd_of_factors_subperm

b6cd9b8

feat(number_theory/padics/padic_norm): div_pow

fe3de83

feat(group_theory/order_of_element): additivize!

d423e26

undo a change I did for debugging

d1f4899

just plain better

22dc2b3

line

32c3589

Merge branch 'dvd_of_factors_subperm' into ericrbg/exponent_lemmas

5ae4e7f

Merge branch 'padic_val_nat.div_pow' into ericrbg/exponent_lemmas

cdae685

feat(group_theory/exponent): exponent G = Sup (range order_of)

6b167e3

ericrbg added help-wanted The author needs attention to resolve issues awaiting-review The author would like community review of the PR labels Dec 13, 2021

github-actions bot added 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 Dec 13, 2021

ericrbg mentioned this pull request Dec 13, 2021

[Merged by Bors] - feat(group_theory/specific_groups/cyclic): |G|=expG ↔ G is cyclic #10692

Closed

1 task

yay finish it

289fbb2

ericrbg removed the help-wanted The author needs attention to resolve issues label Dec 13, 2021

ericrbg added 3 commits December 13, 2021 21:59

spacing

c99a719

dedup lemma

b41f030

add docs

bd06c3f

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 14, 2021

ericrbg added 3 commits December 14, 2021 09:28

Merge branch 'master' into padic_val_nat.div_pow

8ce4eac

Merge branch 'padic_val_nat.div_pow' into ericrbg/exponent_lemmas

86c0955

add an extra version

c89bc24

github-actions bot 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 Dec 14, 2021

ericrbg added 2 commits December 14, 2021 13:03

Merge branch 'master' into order_of_additive

fdf5b33

Merge branch 'order_of_additive' into ericrbg/exponent_lemmas

d663777

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 14, 2021

Julian-Kuelshammer reviewed Dec 14, 2021

View reviewed changes

src/group_theory/exponent.lean Outdated Show resolved Hide resolved

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 15, 2021

ericrbg added 2 commits December 17, 2021 00:41

Merge branch 'master' into ericrbg/exponent_lemmas

27e872b

few more fixes

2fe2b58

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 17, 2021

ericrbg added 3 commits December 17, 2021 15:06

rename

6aecd72

dot notation test

e1d8ff7

remove a finished todo!

d967662

jcommelin reviewed Dec 18, 2021

View reviewed changes

src/group_theory/exponent.lean Outdated Show resolved Hide resolved

ericrbg and others added 2 commits December 18, 2021 09:37

Update src/group_theory/exponent.lean

7767754

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

fix a weird proof

7aab462

jcommelin reviewed Dec 18, 2021

View reviewed changes

extract subproof

c9f3890

speedup

0c64ca4

ericrbg commented Dec 22, 2021

View reviewed changes

tiny golf

7666489

urkud reviewed Dec 23, 2021

View reviewed changes

ericrbg added 2 commits December 23, 2021 11:33

use supr

af7fdfe

update names

612c048

ericrbg changed the title ~~feat(group_theory/exponent): exponent G = Sup (range order_of)~~ feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g Dec 23, 2021

jcommelin approved these changes Dec 23, 2021

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 23, 2021

bors bot pushed a commit that referenced this pull request Dec 23, 2021

feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g (#10767)

e6f4852

Precursor to #10692. Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>

bors bot changed the title ~~feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g~~ [Merged by Bors] - feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g Dec 23, 2021

bors bot closed this Dec 23, 2021

bors bot deleted the ericrbg/exponent_lemmas branch December 23, 2021 20:58

ericrbg mentioned this pull request Aug 21, 2022

[Merged by Bors] - chore(algebra/order/with_zero): Move unrelated lemmas #15676

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g #10767

[Merged by Bors] - feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g #10767

ericrbg commented Dec 13, 2021 •

edited by github-actions bot

ericrbg commented Dec 13, 2021

github-actions bot commented Dec 14, 2021

Julian-Kuelshammer Dec 14, 2021

ericrbg Dec 17, 2021

jcommelin Dec 18, 2021

ericrbg Dec 18, 2021

jcommelin Dec 18, 2021

ericrbg Dec 18, 2021

ericrbg Dec 18, 2021 •

edited

jcommelin commented Dec 22, 2021

ericrbg commented Dec 22, 2021 •

edited

ericrbg Dec 22, 2021

urkud Dec 23, 2021

ericrbg Dec 23, 2021 •

edited

ericrbg Dec 23, 2021 •

edited

jcommelin left a comment

bors bot commented Dec 23, 2021


		variable [cancel_comm_monoid G]

		@[to_additive] lemma exponent_eq_Sup_order_of (h : ∀ g : G, 0 < order_of g) :

[Merged by Bors] - feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g #10767

[Merged by Bors] - feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g #10767

Conversation

ericrbg commented Dec 13, 2021 • edited by github-actions bot

ericrbg commented Dec 13, 2021

github-actions bot commented Dec 14, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ericrbg Dec 18, 2021 • edited

Choose a reason for hiding this comment

jcommelin commented Dec 22, 2021

ericrbg commented Dec 22, 2021 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ericrbg Dec 23, 2021 • edited

Choose a reason for hiding this comment

ericrbg Dec 23, 2021 • edited

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Dec 23, 2021

ericrbg commented Dec 13, 2021 •

edited by github-actions bot

ericrbg Dec 18, 2021 •

edited

ericrbg commented Dec 22, 2021 •

edited

ericrbg Dec 23, 2021 •

edited

ericrbg Dec 23, 2021 •

edited