Transporting the Klein four property along isomorphisms #
Being a Klein four-group, that is having order four and exponent two, is invariant under group isomorphism.
Main results #
MulEquiv.isKleinFour: a group isomorphic to a Klein four-group is a Klein four-group.
theorem
MulEquiv.isKleinFour
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
[IsKleinFour G]
(e : G ≃* H)
:
A group isomorphic to a Klein four-group is a Klein four-group.
theorem
AddEquiv.isAddKleinFour
{G : Type u_1}
{H : Type u_2}
[AddGroup G]
[AddGroup H]
[IsAddKleinFour G]
(e : G ≃+ H)
:
An additive group isomorphic to a Klein four-group is a Klein four-group.