# Zulip Chat Archive

## Stream: new members

### Topic: How to define the order of an element for non-finite groups?

#### Ariel Fridman (Feb 17 2021 at 14:45):

I am learning how to use lean 3 by solving Dummit & Foote's Abstract Algebra.

I am also not using mathlib's `group`

or `group_theory`

modules, since I want to do everything myself (C will do that to ya ^^').

In D&F, the order of an element g is defined as the smallest natural number n for which g^n = 1, or \infty if such a number doesn't exist.

I've looked at the mathlib implementation, and it looks like the order there is defined only for finite groups, which is unsuitable for my needs.

Any tips about how would one go about implementing an order function that does what I need?

#### Johan Commelin (Feb 17 2021 at 14:48):

Yes, this ought to be refactored in mathlib

#### Kevin Buzzard (Feb 17 2021 at 14:49):

I think that a better definition would be that the "order" of an element of infinite order should be 0.

#### Kevin Buzzard (Feb 17 2021 at 14:50):

Then the natural map from the integers to G sending 1 to g has kernel principal generated by `order g`

.

#### Johan Commelin (Feb 17 2021 at 14:51):

```
open_locale classical
noncomputable def order_of' {G : Type*} [group G] (g : G) : ℕ :=
if h : ∃ n : ℕ, 0 < n ∧ g ^ n = 1 then nat.find h else 0
```

#### Johan Commelin (Feb 17 2021 at 14:52):

We just need someone with the time and energy to rewrite that part of mathlib

#### Yakov Pechersky (Feb 17 2021 at 14:54):

Is it possible to case on `fintype`

or not?

#### Ariel Fridman (Feb 17 2021 at 14:55):

Thank you!

Just to see that I understand how this works:

It tries to check if there exists an n: N which is the order of g, and finds it, or otherwise returns zero.

But how does it know if a proof of that exists (aka, h exists)? Does it make me provide a proof of that when I try t assert that the order of g is 5 (for example)?

#### Kevin Buzzard (Feb 17 2021 at 14:57):

Twitter rant : https://twitter.com/XenaProject/status/1301802013278318593?s=20

Here's a funny thing. The set** of ideals of the integers is canonically isomorphic to the natural numbers {0, 1, 2...}. Ideals have a multiplication and it agrees with natural number multiplicatuon. Ideals also have an addition -- and it doesn't! Can we use this? ** Type 1/n

- The Xena Project (@XenaProject)#### Kevin Buzzard (Feb 17 2021 at 14:58):

You shouldn't worry about the definition, because as well as the definition you need an API for the definition -- that would be part of the refactoring.

#### Kevin Buzzard (Feb 17 2021 at 14:58):

For example if G was a finite group then Lean would know that some n existed (e.g. the order of G)

#### Johan Commelin (Feb 17 2021 at 15:12):

@Ariel Fridman If you want to prove `order_of' g = 5`

you will need to show that `g ^ 5 = 1`

and you will need to show that `g ^ 1 ... g ^ 4`

are not `1`

.

#### Johan Commelin (Feb 17 2021 at 15:13):

Of course there is redundance there, so you will want helper lemmas that make your life easier.

#### Johan Commelin (Feb 17 2021 at 15:14):

E.g., a lemma that says that `order_of' g = n`

iff `g ^ n = 1`

and `g ^ k \ne 1`

for all *proper* divisors `k`

of `n`

.

#### Ariel Fridman (Feb 17 2021 at 15:15):

@Johan Commelin I see. Thanks!

#### Kevin Buzzard (Feb 17 2021 at 15:20):

Note that that statement, once corrected to "all proper divisosrs k of n", remains true for n=0 with my convention ;-)

#### Ariel Fridman (Feb 17 2021 at 15:50):

I am probably dense, because I can't seem to be able to prove even simple statements using this definition ^^'.

What I am trying to prove:

```
noncomputable def order_of' {G : Type*} [group G] (g : G) : ℕ :=
if h : ∃ n : ℕ, 0 < n ∧ g ^ n = 1 then nat.find h else 0
notation `|` g `|` := order_of' g
example {G: Type*} [group G] (g: G) : g = 1 → |g| = 1 := sorry
```

I tried providing a term of type `∃ n : ℕ , 0 < n ∧ g^n = 1`

, which was quite easy to prove, but that wasn't it.

Could you please explain what exactly an I supposed to provide/prove, or at least point me in the direction of some docs in which its explained?

#### Ariel Fridman (Feb 17 2021 at 15:52):

and if possible, the same for the other direction (i.e. `|g| = 1 → g = 1`

), since I also haven't been able to see on how to `case`

on it, or desugar it.

#### Yakov Pechersky (Feb 17 2021 at 16:01):

What are your imports?

#### Shing Tak Lam (Feb 17 2021 at 16:03):

```
import algebra.group.basic
import data.nat.enat
import tactic.interval_cases
variables {G : Type*} [group G]
open_locale classical
noncomputable def order_of' {G : Type*} [group G] (g : G) : ℕ :=
if h : ∃ n : ℕ, 0 < n ∧ g ^ n = 1 then nat.find h else 0
notation `|` g `|` := order_of' g
example (g : G) : |(1 : G)| = 1 :=
begin
unfold order_of',
have h : ∃ n, 0 < n ∧ (1 : G) ^ n = 1,
{ use [1, zero_lt_one, one_pow _] },
rw dif_pos h,
rw nat.find_eq_iff,
split,
{ simp },
{ intros n hn hc,
cases hc with h1 h2,
interval_cases n }
end
example (g : G) (hg : |g| = 1) : g = 1 :=
begin
unfold order_of' at hg,
split_ifs at hg,
{ have := nat.find_spec h,
cases this with h1 h2,
rwa [hg, pow_one] at h2 },
{ contradiction }
end
```

(obviously can be golfed)

#### Ariel Fridman (Feb 17 2021 at 16:04):

Yakov Pechersky said:

What are your imports?

just `tactic`

and `init.data.int`

. I don't actually use `group`

, but rather a typeclass I made myself called `Group`

.

#### Ariel Fridman (Feb 17 2021 at 16:05):

@Shing Tak Lam Thank you!, I'll look at it and try to understand what you're doing.

#### Johan Commelin (Feb 17 2021 at 16:16):

@Ariel Fridman The definition uses `nat.find`

, so you will have to use lemmas about `nat.find`

.

#### Johan Commelin (Feb 17 2021 at 16:17):

If you `Ctrl-click`

on it (assuming you are using VScode as editor), then you will go to the definition.

#### Johan Commelin (Feb 17 2021 at 16:17):

Just below it will be 10 useful lemmas for using it

#### Bryan Gin-ge Chen (Feb 17 2021 at 16:20):

Note that you usually don't have to import anything that starts with `init`

, all of that comes "for free" in every Lean file, unless you put `prelude`

at the top of your file. If you do happen to have `prelude`

at the top of your file, you would have gotten everything in `init`

by importing `tactic`

.

#### Ariel Fridman (Feb 17 2021 at 16:28):

@Johan Commelin I'll take a look at it, thanks!

#### Ariel Fridman (Feb 17 2021 at 16:29):

@Bryan Gin-ge Chen and thank you for this tip. so `init`

just an autoinclude prelude? I assumed it was part of mathlib, but I guess I was wrong.

#### Bryan Gin-ge Chen (Feb 17 2021 at 16:35):

Yep, everything in `init.`

is part of what we call "core Lean", and can be found in the community Lean 3 repository here.

Last updated: Dec 20 2023 at 11:08 UTC