order of element

Stream: new members

[Alena Gusakov]

So I'd like to prove some things about the order of an element of a group. Based on the definitions/lemmas in group_theory/order_of_element, it seems like what's happening is the group is simply declared as finite, which forces the elements to have finite order. What I'd like to know is whether there's a way to declare some element a : G for (possibly infinite) group G such that order_of a exists, i.e. it's finite. Would I have to grab a finite subgroup of G in order to do that, or is there another way?

[Alena Gusakov]

(sorry this might be a question that belongs in #Is there code for X? now that I think about it)

[Kevin Buzzard]

Is it not the case that there's a function which works in general and returns 0 if it has infinite order?

[Kevin Buzzard]

The cunning way to do the order of an element $g$ of a group $G$ in general is to consider the kernel of the map $\mathbb{Z}\to G$ sending $n$ to $g^n$.

[Kevin Buzzard]

It's principal with a canonical generator.

[Jalex Stark]

i don't see the function kevin is asking about anywhere nearby docs#order_of

[Jalex Stark]

but the approach used there will let you define order_of on anything for which you can prove is torsion

[Alena Gusakov]

I guess what I'm trying to prove is more like, if there exists some element of G of finite order n, then...etc

[Alena Gusakov]

So it's like, in general, I'm trying to construct the statement order_of a = n → something regardless of whether there actually is an element of finite order in the given group

[Alena Gusakov]

If the group has no elements of finite order besides the identity, the thing I want to prove is trivially true so it technically is a true statement regardless of whether the group is finite

[Jalex Stark]

yes, i think the things you're saying mean the same thing I said. You can look at the implementation of order_of_element and add an extra hypothesis ∃ n, x ^ n = 1

[Jalex Stark]

all of the proofs will go through, changing at most one line in each one

[Jalex Stark]

maybe I don't know where you are stuck

[Alena Gusakov]

Ah gotcha, that works. Thanks!

[Jalex Stark]

and this clearly belongs in mathlib, but I don't know how one would organize it