Revision #1337 → #2113 · back to history
modifiedIsomorphic to dihedral group of order 471f458b93850
| Field | From #1337 | To #2113 |
|---|
| mathlib.decl | DihedralGroup.instIsKleinFour | DihedralGroup.instIsKleinFourOfNatNat |
| note | The instance `IsKleinFour (DihedralGroup 2)` combined with `IsKleinFour.nonempty_mulEquiv` gives the isomorphism with any Klein four-group. | The anonymous instance `IsKleinFour (DihedralGroup 2)` (auto-named `DihedralGroup.instIsKleinFourOfNatNat`) combined with `IsKleinFour.nonempty_mulEquiv` gives the isomorphism with any Klein four-group. |
addedOnly abelian dihedral group besides order 205c2a8c8d32d
modifiedIsomorphic to direct sum Z2⊕Z26ddb57cc76ae
| Field | From #1337 | To #2113 |
|---|
| mathlib.decl | IsAddKleinFour.instZModProd | instIsAddKleinFourProdZModOfNatNat |
| note | The instance `IsAddKleinFour (ZMod 2 × ZMod 2)` together with `IsAddKleinFour.nonempty_addEquiv` provides the isomorphism. | The anonymous instance `IsAddKleinFour (ZMod 2 × ZMod 2)` (auto-named `instIsAddKleinFourProdZModOfNatNat`) together with `IsAddKleinFour.nonempty_addEquiv` provides the isomorphism. |
addedTransitive subgroup of S_4 as a Galois groupd1752198d087
addedKernel of S_4 → S_3911a55de6e56
addedQuotient of units of split-complex numbersed041f73d61d