mathlib

1983e40a - feat(data/zmod/basic): If the orbit is finite, then the minimal period is positive (#14201)

feat(data/zmod/basic): If the orbit is finite, then the minimal period is positive (#14201) This PR adds an instance stating that if the orbit is finite, then the minimal period is positive. The instance is needed for an explicit computation that involves a product indexed by `zmod (minimal_period ((•) a) b)`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>