order of a group

Stream: new members

[Luca Seemungal]

Hi,

I can't seem to find for the life of me the definition of the order of a group in mathlib - can anyone point this out to me? Additionally, is there some easy way of finding out stuff like this (without asking here) that I don't know about?

Many thanks

[Kevin Buzzard]

Groups aren't anything special -- you want to know how to find the order of a type, right?

[Kevin Buzzard]

What type do you want the answer to be?

[Luca Seemungal]

a natural number or infinity

[Kevin Buzzard]

Because you could have said "a cardinal" (which is a much more refined answer, where there are all sorts of different kinds of infinities)

[Kevin Buzzard]

or you could have said "Oh I am only interested in finite groups, so a natural number"

[Kevin Buzzard]

and in Lean these are all different functions because they map to different types

[Luca Seemungal]

I see - thanks! I think group.sizeof is something I want

Another thing - what is the order of an element of a group? (as in, what is it in mathlib, not what is it in maths)

[Kevin Buzzard]

What is the type of the value you want returned?

[Alex Mathers]

here's one place to look: https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/order_of_element.lean

[Luca Seemungal]

I think I'll start with elements of finite order haha

[Luca Seemungal]

Oh thanks!

[Kevin Buzzard]

The answers to your questions depend on which domain you want to apply them in. If you are working with all groups then you need one function, if you're working with finite groups then you need a different function because now the answer can't be $\infty$. Then you might find that some computer scientist has come along and decreed that actually it's OK because if an element does have infinite order then we may as well just say it has order 0 or 37 and then we have an order function which takes values in the natural number and works even if the elements have infinite order, it just gives the wrong answer

[Kevin Buzzard]

In short, the questions you're asking sound mathematically fine but formally they are sufficiently vague for the answer actually to be "well there are several functions which do an approximation to what you are asking in different situations"

[Luca Seemungal]

Ah right I see

I'm not very used to this, hopefully it'll become more obvious when I'm making a huge number of assumptions

[Alex J. Best]

Luca Seemungal said:

I see - thanks! I think group.sizeof is something I want

Another thing - what is the order of an element of a group? (as in, what is it in mathlib, not what is it in maths)

group.sizeof is not what you want for example #eval add_group.sizeof (zmod 4) $ add_comm_group.to_add_group (zmod 4) returns 1.

[Scott Morrison]

All the .sizeof functions are essentially internal type-theoretic implementation details.

[Scott Morrison]

They probably should have been called ._sizeof or something to make it clearer.