Stream: math-comp users

Topic: ✔ Semidirect Product


view this post on Zulip Cyril Cohen (May 23 2023 at 13:36):

You should start from unit (which is in Set) instead of True (which is in Prop and the reason why you have problems here, I believe). And indeed you can equip it with a fingroup type if you want (it is already a finite type in the library). Otherwise if you're just looking for any fingroup with one element, you could also use either {perm unit}(the permutations of the type unit with a single element) or {unit bool} (the type of inversible elements (a.k.a. units) of the ring of booleans).

view this post on Zulip Notification Bot (May 23 2023 at 13:43):

Raül has marked this topic as resolved.


Last updated: Jul 15 2024 at 20:02 UTC