Subgroups of zmod

Stream: Is there code for X?

[Yaël Dillies]

Is there a characterisation of the subgroups of docs#zmod? What I need precisely is that for n ≠ 0, the smallest nontrivial subgroup of zmod n has size n.min_fac.

[Yaël Dillies]

I would expect an order_iso between subgroup (zmod n) and Icc 1 n in the divisibility order.

[Kevin Buzzard]

Your first statement doesn't work for n=1 either but the last one works for all n if you add an op

[Yaël Dillies]

Why adding an op? Icc 1 n admits an order-reversing isomorphism.

[Kevin Buzzard]

Not if n=0

[Yaël Dillies]

Good point

[Kevin Buzzard]

You are using "order of subgroup" and I'm using "smallest generator"

[Eric Rodriguez]

The API for cyclic groups is pretty shambolic, sadly

[Yaël Dillies]

Do we have a type synonym for the divisibility preorder associated to a monoid, at least?

[Eric Wieser]

No, but we might have a def somewhere that makes the instance you want

[Eric Wieser]

A type synonym sounds like a good idea though