nonempty_mulEquiv — Mathlib

English

Any two Klein four groups are isomorphic; in particular there exists a multiplicative isomorphism between them.

Русский

Любые две группы Klein четверки изоморфны; в частности существует мультипликативная изоморфия между ними.

LaTeX

$$$\forall G_1, G_2\,[\text{IsKleinFour}(G_1)]\,[\text{IsKleinFour}(G_2)],\; \exists\phi: G_1 \cong^* G_2$$$

Lean4

/-- Any two `IsKleinFour` groups are isomorphic. -/
@[to_additive /-- Any two `IsAddKleinFour` groups are isomorphic. -/
    ]
theorem nonempty_mulEquiv [IsKleinFour G₂] : Nonempty (G₁ ≃* G₂) := by
  classical
  let _inst₁ := Fintype.ofFinite G₁
  let _inst₁ := Fintype.ofFinite G₂
  exact ⟨mulEquiv ((Fintype.equivOfCardEq <| by simp).setValue 1 1) <| by simp⟩

Похожие утверждения