Is there a tutorial for getting started with fingroup? Currently I'm getting stuck trying to define the type of elements of a cyclic group on a generator, something like `{x | x \in <[g]>}`

IIRC `<[g]>`

is already a `{group gT}`

, so `[subg <[g]>]`

should be enough. Is this what you are looking for?

Indeed, thank you.

How do I get a `choiceType`

from `<[g]>`

?

Got it, `subg_choiceType (<[g]>)%G`

worked.

Right, but that should be inferred automatically for the type I wrote. See also the notation [choiceType of ...] (There is one per structure, eq.. choice...fin...)

All this is briefly described here https://math-comp.github.io/mcb

(chapter 6.10 for the `[someStructure of ...]`

and 7 for the subtype construction)

i'd love codebases of example usage, projects that depend on mathcomp's fingroups. I grepped around the book pdf for cyclic, finite group, etc. there wasn't anything.

for example, https://github.com/math-comp/odd-order and https://github.com/math-comp/Abel depend on fingroup

Last updated: Jul 25 2024 at 15:02 UTC