Theorems · Inductive type · group theory

AddSubgroup.Normal

{A : Type u_2} → [inst : AddGroup A] → AddSubgroup A → Prop

An AddSubgroup H is normal if whenever n ∈ H, then g + n - g ∈ H for every g : A [Wikidata Q743179](https://www.wikidata.org/wiki/Q743179)

Defined in

Mathlib.Algebra.Group.Subgroup.Defs

Cited by

183 results in Mathlib

Foundations

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

Assumes

AddGroup