Commit 2023-11-30 19:19 1b08a550

feat: abstract KleinFour into a class IsKleinFour. (#8565) This removes KleinFour in favor of a class IsKleinFour and proves that any two IsKleinFour groups are isomorphic via any identity-preserving equivalence. In addition, we prove that a group of order 4 is not cyclic if and only if it has exponent two. There are several advantages:

1. this provides a general API accessible by other groups
2. we prove some generic facts about groups of exponent two
3. it is easy to @[to_additive] everything If we want, we can always redefine an explicit KleinFour group, and give it an IsKleinFour instance. In that case we probably want to make a bespoke type for it, so that it can be to_additive-ized.