Stream: math-comp users

Topic: getting started with fingroup


view this post on Zulip 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]>}

view this post on Zulip 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?

view this post on Zulip Philipp G. Haselwarter (Dec 10 2020 at 16:16):

Indeed, thank you.

view this post on Zulip Philipp G. Haselwarter (Dec 10 2020 at 18:02):

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

view this post on Zulip Philipp G. Haselwarter (Dec 10 2020 at 18:06):

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

view this post on Zulip 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...)

view this post on Zulip Enrico Tassi (Dec 10 2020 at 22:44):

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

view this post on Zulip 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