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)

Last updated: Jan 29 2023 at 19:02 UTC