OAI/Topology/ArtinGroups/ParabolicIntersections/TreeMinimalNormal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A minimal segment stabilizer in a branching tree action is normal when adjacent vertex stabilizers generate the acting group.

  1. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.minimal_pair_normal line 13