isSimpleGroup — Mathlib

English

A group G is simple if and only if it is isomorphic to a simple group H.

Русский

Группа G простая тогда и только тогда, когда она изоморфна простой группе H.

LaTeX

$$IsSimpleGroup G ↔ IsSimpleGroup H$$

Lean4

@[to_additive]
theorem _root_.MulEquiv.isSimpleGroup {H : Type*} [Group H] [IsSimpleGroup H] (e : G ≃* H) : IsSimpleGroup G :=
  haveI : Nontrivial G := e.toEquiv.nontrivial
  isSimpleGroup_of_surjective e.symm.toMonoidHom e.symm.surjective

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