Subgroup.Normal.eq_bot_or_eq_top
theorem Subgroup.Normal.eq_bot_or_eq_top :
∀ {G : Type u_1} [inst : Group G] [inst_1 : IsSimpleGroup G] {H : Subgroup G}, H.Normal → H = ⊥ ∨ H = ⊤
This theorem states that for any group `G` that is a simple group, any `H` which is a normal subgroup of `G` must be either the trivial group (denoted by `⊥`) or the entire group `G` itself (denoted by `⊤`). This is a special property of simple groups which have no non-trivial normal subgroups.
More concisely: In a simple group, every normal subgroup is either the trivial group or the entire group.
|
IsSimpleAddGroup.eq_bot_or_eq_top_of_normal
theorem IsSimpleAddGroup.eq_bot_or_eq_top_of_normal :
∀ {A : Type u_2} [inst : AddGroup A] [self : IsSimpleAddGroup A] (H : AddSubgroup A), H.Normal → H = ⊥ ∨ H = ⊤ := by
sorry
This theorem states that for a given additive group 'A' that is simple (i.e., has no nontrivial normal subgroups), any normal subgroups 'H' of 'A' is either the bottom (`⊥`, meaning the trivial subgroup consisting only of the identity element) or the top (`⊤`, meaning the entire group 'A' itself).
More concisely: In a simple additive group 'A', every normal subgroup is either the trivial subgroup or the entire group itself.
|
IsSimpleGroup.eq_bot_or_eq_top_of_normal
theorem IsSimpleGroup.eq_bot_or_eq_top_of_normal :
∀ {G : Type u_1} [inst : Group G] [self : IsSimpleGroup G] (H : Subgroup G), H.Normal → H = ⊥ ∨ H = ⊤
This theorem states that for any simple group `G`, any normal subgroup `H` of `G` is either the trivial subgroup `⊥` (consisting of only the identity element) or the entire group `G` itself, denoted by `⊤`. In other words, in the context of simple groups, normal subgroups can only be either trivial or the whole group.
More concisely: In a simple group, every normal subgroup is either the trivial subgroup or the entire group.
|