Theorems · Definition · group theory

AddSubgroup.inertia

{M : Type u_6} → [inst : AddGroup M] → AddSubgroup M → (G : Type u_7) → [inst : Group G] → [MulAction G M] → Subgroup G

Suppose G acts on M and I is a subgroup of M. The inertia subgroup of I is the subgroup of G whose action is trivial mod I.

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

6 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

AddGroupGroupMulAction