lean_workbook_plus_42412

Proved

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

Let $H$ be a subgroup of finite index of an infinite group $G$ . Prove that $G$ has a normal subgroup of finite index which is contained in $H$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42412 (G : Type*) [Group G] [Infinite G]
    (H : Subgroup G) [H.FiniteIndex] : ∃ N : Subgroup G, N.Normal ∧ N.FiniteIndex ∧ N ≤ H   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph