# Zulip Chat Archive

## Stream: new members

### Topic: order of element

#### Alena Gusakov (Jun 24 2020 at 22:47):

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 (Jun 24 2020 at 22:49):

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

#### Kevin Buzzard (Jun 24 2020 at 22:50):

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

#### Kevin Buzzard (Jun 24 2020 at 22:51):

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 (Jun 24 2020 at 22:51):

It's principal with a canonical generator.

#### Jalex Stark (Jun 24 2020 at 22:59):

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

#### Jalex Stark (Jun 24 2020 at 23:00):

but the approach used there will let you define `order_of`

on anything for which you can prove is torsion

#### Alena Gusakov (Jun 25 2020 at 01:05):

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 (Jun 25 2020 at 01:14):

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 (Jun 25 2020 at 01:17):

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 (Jun 25 2020 at 01:39):

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 (Jun 25 2020 at 01:40):

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

#### Jalex Stark (Jun 25 2020 at 01:41):

maybe I don't know where you are stuck

#### Alena Gusakov (Jun 25 2020 at 01:46):

Ah gotcha, that works. Thanks!

#### Jalex Stark (Jun 25 2020 at 01:57):

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

Last updated: May 14 2021 at 22:15 UTC