Commit 2021-03-17 08:30 6f6b548b

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.