quotient): `orbit (zpowers a) b` is a cycle of order `minimal_period ((•) a) b` (#14124)

Commit

3 years ago

feat(data/zmod/quotient): `orbit (zpowers a) b` is a cycle of order `minimal_period ((•) a) b` (#14124) This PR applies the orbit-stabilizer theorem to the action of a cyclic subgroup.

Author

tb65536

Parents

bc7a201e

mathlib 55b31e05 - feat(data/zmod/quotient): `orbit (zpowers a) b` is a cycle of order `minimal_period ((•) a) b` (#14124)

mathlib
55b31e05 - feat(data/zmod/quotient): `orbit (zpowers a) b` is a cycle of order `minimal_period ((•) a) b` (#14124)