Theorems · Inductive type · group theory

Subgroup.Normal

{G : Type u_1} → [inst : Group G] → Subgroup G → Prop

A subgroup H is normal if whenever n ∈ H, then g * n * g⁻¹ ∈ H for every g : G [Wikidata Q743179](https://www.wikidata.org/wiki/Q743179)

Defined in

Mathlib.Algebra.Group.Subgroup.Defs

Cited by

334 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms

Assumes

Group