issue #1563: order of element

Stream: triage

[Random Issue Bot]

Today I chose issue 1563 for discussion!

order of element
Created by @Johan Commelin (@jcommelin) on 2019-10-17
Labels: easy, needs-refactor

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 1563 for discussion!

order of element
Created by @Johan Commelin (@jcommelin) on 2019-10-17
Labels: easy, needs-refactor

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

A bunch of theorems in that file are true for infinite groups if you define the order of an element of infinite order to be 0. I'm surprised that this was not the convention chosen by Johannes.

[Kevin Buzzard]

Even more are true if you use fincard (the cardinal of an infinite set being 0)

[Julian Külshammer]

I recently looked at this issue and was confused as to why the order of an element is only defined for finite groups. This seems like it wouldn't scale well in the future.

[Kevin Buzzard]

One issue is that nat is much easier to work with than enat (:= $\mathbb{N}\cup\{\infty\}$), and lean likes total functions. The rather esoteric solution of letting elements of infinite order have order 0 looks weird to mathematicians but actually works really nicely, and this is because a conceptual way of thinking about the order of g is the kernel of the map from Z to G sending 1 to g; this kernel has a unique nonnegative generator which one could define to be the order.

[Julian Külshammer]

Another question I had regarding this issue was why the characteristic of a ring is not defined as the order of 1? If one defined the order here as zero if infinite, then this would also agree with characteristic 0.

[Kevin Buzzard]

I agree that this would be a nice way to do it! Perhaps the answer is simply that it was done another way and we now have an API which works, so why change it? It doesn't really matter what the definitions are as long as the API is there.