Zulip Chat Archive
Stream: triage
Topic: PR #8632: feat(group_theory/p_group): Groups of order p^2...
Random Issue Bot (Jan 20 2022 at 14:16):
Today I chose PR 8632 for discussion!
feat(group_theory/p_group): Groups of order p^2 are commutative
Created by @Chris Hughes (@ChrisHughes24) on 2021-08-11
Labels: awaiting-review, awaiting-author
Is this PR still relevant? Any recent updates? Anyone making progress?
Alex J. Best (Jan 20 2022 at 17:41):
This is now please-adopt and good-first-project! If someone wants to take on fixing the errors / cleaning this up and getting it merged it would be a nice contribution :smile:
Random Issue Bot (Mar 23 2022 at 14:13):
Today I chose PR 8632 for discussion!
feat(group_theory/p_group): Groups of order p^2 are commutative
Created by @Chris Hughes (@ChrisHughes24) on 2021-08-11
Labels: please-adopt, good-first-project
Is this PR still relevant? Any recent updates? Anyone making progress?
Alex J. Best (Mar 23 2022 at 20:58):
@Jakub Kądziołka was thinking about this, https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/groups.20of.20order.20p.C2.B2/near/274818378 not sure what happened
Random Issue Bot (May 14 2022 at 14:20):
Today I chose PR 8632 for discussion!
feat(group_theory/p_group): Groups of order p^2 are commutative
Created by @Chris Hughes (@ChrisHughes24) on 2021-08-11
Labels: please-adopt, good-first-project
Is this PR still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (May 14 2022 at 15:17):
Oh I could see if I could find UGs to finish this one.
Thomas Browning (May 14 2022 at 17:26):
Mathlib already has knows that p-groups have nontrivial center, that groups of order p are cyclic, and that if the quotient by the center is cyclic, then the group is abelian. So it should just be a matter of putting the pieces together.
Yaël Dillies (May 14 2022 at 17:36):
Isn't that exactly what this PR is doing?
Thomas Browning (May 15 2022 at 01:33):
Pretty much, but mathlib has grown in the past 9 months, so it might be even easier than the proof in the PR. For example,exists_ne_one_mem_center shouldn't be needed now, since we have docs#is_p_group.bot_lt_center.
Riccardo Brasca (May 15 2022 at 12:52):
@Brendon James Thomson you were interested in this, right?
Brendon James Thomson (May 15 2022 at 16:07):
yup!
Last updated: Dec 20 2023 at 11:08 UTC