English
Let G1 and G2 be Klein four groups. For any equivalence e: G1 ≃ G2 with e(1) = 1, there exists a multiplicative isomorphism G1 ≅* G2.
Русский
Пусть G1 и G2 — группы Klein четверки. Для любой эквивалентности e: G1 ≃ G2 such that e(1) = 1 существует мультипликативная изоморфия G1 ≅* G2.
LaTeX
$$$\forall G_1, G_2 \, [\text{IsKleinFour}(G_1)]\,[\text{IsKleinFour}(G_2)],\; \exists e: G_1 \to G_2,\ e(1)=1 \Rightarrow G_1 \cong^* G_2$$$
Lean4
/-- Any two `IsKleinFour` groups are isomorphic via any equivalence which sends the identity of one
group to the identity of the other. -/
@[to_additive /-- Any two `IsAddKleinFour` groups are isomorphic via any
equivalence which sends the identity of one group to the identity of the other. -/
]
abbrev mulEquiv [IsKleinFour G₂] (e : G₁ ≃ G₂) (he : e 1 = 1) : G₁ ≃* G₂ :=
mulEquiv' e he exponent_two
