OAI/Topology/ArtinGroups/ParabolicIntersections/WeakMalnormalAlgebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conjugation and subgroup facts about weak malnormality.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.weaklyMalnormal_of_conjugates_inf_bot line 9
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal.mono line 17
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal.conjugate_subgroup line 22