Existence of elements of order p in a group

Stream: Is there code for X?

[Michael Stoll]

Does mathlib have the statement that in a finite (additive) group whose order is divisible by a prime p, there exists an element of order p?
I have no idea what such a lemma would be named and haven't found something when looking through some files in algebra/group or group_theory.

[Junyan Xu]

Not sure about that exact statement but we have https://leanprover-community.github.io/mathlib_docs/group_theory/sylow.html

[Junyan Xu]

docs#sylow.exists_subgroup_card_pow_prime_le should be directly applicable

[Michael Stoll]

Does this also exist for add_groups?

[Michael Stoll]

To go via multiplicative is likely rather painful...

[Junyan Xu]

There is docs#subgroup.to_add_subgroup

[Junyan Xu]

Maybe you want docs#subgroup.to_add_subgroup' and docs#add_subgroup.to_subgroup

[Junyan Xu]

It seems the Sylow theorems aren't to_additive'd.

[Alex J. Best]

There is the very oddly named docs#equiv.perm.exists_prime_order_of_dvd_card which also has no to_additive and no docstring calling it "Cauchy's theorem" :oh_no:

[Alex J. Best]

There is a docstring in the file header with the word "Cauchy`s" (note the backtick so searching for "Cauchy's theorem" doesnt work) but as there are many references to Cauchy in mathlib just looking for "Cauchy" gives way too many results

[Michael Stoll]

Thanks; this gives at least the multiplicative version. exists_prime_order_of_dvd_card is natural enough, only the prefix is a bit weird...

[Michael Stoll]

Using docs#equiv.perm.exists_prime_order_of_dvd_card, the pain is bearable:

import group_theory.perm.cycle.type

lemma add_group.exists_prime_order_of_dvd_card (G : Type*) [add_group G] [fintype G]
 {p : ℕ} [fact p.prime] (hp : p ∣ fintype.card G) : ∃ g : G, add_order_of g = p :=
begin
  change p ∣ fintype.card (multiplicative G) at hp,
  exact equiv.perm.exists_prime_order_of_dvd_card p hp,
end

[Alex J. Best]

I would add this below the existing one

lemma exists_prime_add_order_of_dvd_card {G : Type*} [add_group G] [fintype G] (p : ℕ)
  [hp : fact p.prime] (hdvd : p ∣ fintype.card G) : ∃ x : G, add_order_of x = p :=
@exists_prime_order_of_dvd_card (multiplicative G) _ _ _ _ hdvd

attribute [to_additive exists_prime_add_order_of_dvd_card] exists_prime_order_of_dvd_card

[Alex J. Best]

But they should probably both not be namespaced imo.

[Michael Stoll]

You are welcome to do it, AFAIC.

[Alex J. Best]

#14471

[Riccardo Brasca]

What prevents to_additive to work automatically here?

[Alex J. Best]

Many things, in this case, even the naive approach of adding to additive to everything in the file fails for some unclear reasons.
But the main reason is really that the theory of permutation groups in lean is completely multiplicative with no additive analogue at present. (equiv.perm is a group and not an add_group)

[Thomas Browning]

Thanks @Alex J. Best for the PR fixing things. Sorry for bungling this so badly in #8916.

[Thomas Browning]

Seems that I created quite the mess with the name, namespace, lack of to_additive, and backtick in Cauchy's. Glad it's all sorted out now.

[Alex J. Best]

No need to be sorry, I think it never had a to additive, and was always in some non-root namespace, so it wasn't just you :wink:, this is the fun of a work in progress collaborative effort after all!
I do wonder if we will ever need sylow-type theorems for add_groups, but we can cross that bridge if we come to it I guess.

[Yaël Dillies]

Yeah, equiv.perm should be treated as a fixed type by to_additive, just as ℕ is. I already reaised this issue several times but apparently no one picked it up. I don't know where you do that but I believe the fix is easy to someone who has hacked on to_additive before.

[Alex J. Best]

But do you think equiv.perm should have a + on it that does the same as *? Because for results whose proofs work by (for example) embedding a multiplicative group into their own equiv.perm as a mul_hom the corresponding additivized result would have to relate to the + on equiv.perm it seems

[Yaël Dillies]

Does that ever happen? If so, can we teach to_additive to insert multiplicative somehow? Sounds fragile :sad:

[Alex J. Best]

I don't remember which specific proofs from that part of group theory use this sort of trick, but I imagine a lot of them do yes.
And yeah its very annoying, this is also why a lot of proofs that use multiplicative nat aren't to_additived currently, to_additive doesn't even know to just remove the multiplicative. Whenever we have an asymmetry like this and the group operation on the fixed type actually interacts with the group one it gets very annoying very quick.

[Violeta Hernández]

Is there no way to transfer statements from additive groups to multiplicative groups and viceversa?

[Violeta Hernández]

I don't know how this would actually work, but given that they're the same algebraic structure with different symbols, it feels like it should be possible...

[Alex J. Best]

There is a gap between possible and already implemented and tested unfortunately, in principle we could have a to_multiplicative the same as to_addtive and many other similar tactics (as suggested in a recent issue) all using the same core code, but nobody has done it and it's not completely trivial to do as to_additive does a lot right now already.

[Sebastien Gouezel]

And it's probably not a good time to implement new bells and whistles on to_additive, because these would also need to be ported to Lean 4.