quotient): The minimal period equals the cardinality of the orbit (#14183)

Commit

3 years ago

feat(data/zmod/quotient): The minimal period equals the cardinality of the orbit (#14183) This PR adds a lemma stating that `minimal_period ((•) a) b = card (orbit (zpowers a) b)`.

Author

tb65536

Parents

3c87882b

mathlib 3d279118 - feat(data/zmod/quotient): The minimal period equals the cardinality of the orbit (#14183)

mathlib
3d279118 - feat(data/zmod/quotient): The minimal period equals the cardinality of the orbit (#14183)