Prove2Me

Subgroup_of_Index_2_is_Normal

Proved

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

group-theoryindexnormal-subgroupproofwiki

A subgroup of index 2 is always normal.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic

theorem Subgroup_of_Index_2_is_Normal {G : Type _} [Group G] (H : Subgroup G) (h : H.index = 2) : H.Normal := by sorry
Source
https://proofwiki.org/wiki/Subgroup_of_Index_2_is_Normal

View graph