Kernel_of_Group_Action_is_Normal_Subgroup

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

group-actionsgroup-theorykernelnormal-subgroupsproofwiki

Let $G$ be a group whose identity is $e$ . Let $X$ be a set. Let $\phi: G \times X \to X$ be a group action. Let $G_0$ denote the kernel of $\phi$ . Then $G_0$ is a normal subgroup of $G$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Kernel_of_Group_Action_is_Normal_Subgroup {G : Type _} [Group G] {X : Type _} [MulAction G X] : (MulAction.toPermHom G X).ker.Normal := by sorry

Source

https://proofwiki.org/wiki/Kernel_of_Group_Action_is_Normal_Subgroup

View graph