OAI/GroupTheory/PolycyclicRecognition/Algebra/MaximalAbelianNormal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Maximal abelian normal subgroups for nilpotent lattice finiteness

  1. theorem OAI.PolycyclicRecognition.exists_maximal_abelian_normal_subgroup line 17
  2. theorem OAI.PolycyclicRecognition.centralizer_eq_of_maximal_abelian_normal line 42

    Source documentation

    In a nilpotent group, a maximal abelian normal subgroup is its own centralizer. This permits a faithful action of the quotient on that subgroup.

    theorem centralizer_eq_of_maximal_abelian_normal [Group.IsNilpotent G]
    (A : Subgroup G) [A.Normal] [IsMulCommutative A]
    (hmax : ∀ B : Subgroup G, B.Normal → IsMulCommutative B → A ≤ B → B = A) :
    Subgroup.centralizer (A : Set G) = A := by
…