Philipp G. Haselwarter (Dec 10 2020 at 15:16): 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