## Stream: math-comp users

### Topic: getting started with fingroup

#### Philipp G. Haselwarter (Dec 10 2020 at 15:16):

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]>}

#### Enrico Tassi (Dec 10 2020 at 16:11):

IIRC <[g]> is already a {group gT}, so [subg <[g]>] should be enough. Is this what you are looking for?

#### Philipp G. Haselwarter (Dec 10 2020 at 16:16):

Indeed, thank you.

#### Philipp G. Haselwarter (Dec 10 2020 at 18:02):

How do I get a choiceType from <[g]> ?

#### Philipp G. Haselwarter (Dec 10 2020 at 18:06):

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

#### Enrico Tassi (Dec 10 2020 at 22:42):

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...)

#### Enrico Tassi (Dec 10 2020 at 22:44):

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

#### Enrico Tassi (Dec 11 2020 at 08:50):

(chapter 6.10 for the [someStructure of ...] and 7 for the subtype construction)

Last updated: Jan 29 2023 at 19:02 UTC