OAI/GroupTheory/FiniteLattice/GeneratedNormality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GeneratedNormality.normal_of_generating_family line 8

   Source documentation

   A subgroup normalized by every member of a generating family is normal.

   theorem normal_of_generating_family
       {K : Type*} [Group K] {ι : Sort*}
       (U : ι → Subgroup K) (hU : (⨆ i, U i) = ⊤)
       (Q : Subgroup K)
       (hn : ∀ i, U i ≤ Subgroup.normalizer (Q : Set K)) : Q.Normal := by
   …