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)

view this post on Zulip Quinn (Nov 13 2023 at 18:07):

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.

view this post on Zulip Karl Palmskog (Nov 14 2023 at 08:17):

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