Theorems · Theorem · group theory

AddSubgroup.le_normalizer_closure_iff

∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {s : Set G},
  H ≤ AddSubgroup.normalizer ↑(AddSubgroup.closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h + g + -h ∈ AddSubgroup.closure s

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

1 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroup