OAI/Topology/ArtinGroups/ParabolicIntersections/NormalizerAlgebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normalizing a subgroup can be tested outside any proper subgroup.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.conjugate_eq_map line 9
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.mem_normalizer_iff_conjugate line 15
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.le_normalizer_of_outside line 21