Quotient_of_Transformation_Group_acts_Effectively

Proved

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

effective-actionsgroup-actionsgroup-theoryproofwikitransformation-groups

Let $G$ be a transformation group (which may or may not be effective) acting on $X$ . Then the quotient group $G / G_0$ , where $G_0$ is the kernel, ''does'' act effectively on $X$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Quotient_of_Transformation_Group_acts_Effectively {G : Type _} [Group G] {X : Type _} [MulAction G X] (h : (MulAction.toPermHom G X).ker = ⊥) : Function.Injective (MulAction.toPermHom G X) := by sorry

Source

https://proofwiki.org/wiki/Quotient_of_Transformation_Group_acts_Effectively

View graph