## 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: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.

#### 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 },
end

(obviously can be golfed)

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

Yakov Pechersky said:

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