Theorems · Definition · group theory

IsAddKleinFour.addEquiv

{G₁ : Type u_2} →
  {G₂ : Type u_3} →
    [inst : AddGroup G₁] →
      [inst_1 : AddGroup G₂] → [IsAddKleinFour G₁] → [IsAddKleinFour G₂] → (e : G₁ ≃ G₂) → e 0 = 0 → G₁ ≃+ G₂

Any two IsAddKleinFour groups are isomorphic via any equivalence which sends the identity of one group to the identity of the other.

Defined in

Mathlib.GroupTheory.SpecificGroups.KleinFour

Cited by

1 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddGroupIsAddKleinFourIsAddKleinFour