# Commit 2021-03-17 08:30 6f6b548b

View on Github →refactor(group_theory/order_of_element): now makes sense for infinite monoids (#6587)
This PR generalises `order_of`

from finite groups to (potentially infinite) monoids. By convention, the value of `order_of`

for an element of infinite order is `0`

. This is non-standard for the order of an element, but agrees with the convention that the characteristic of a field is `0`

if `1`

has infinite additive order. It also enables to remove the assumption `0<n`

for some lemmas about orders of elements of the dihedral group, which by convention is also the infinite dihedral group for `n=0`

.
The whole file has been restructured to take into account that `order_of`

now makes sense for monoids. There is still an open issue about adding [to_additive], but this should be done in a seperate PR. Also, some results could be generalised with assumption `0 < order_of a`

instead of finiteness of the whole group.