VisualEdgeMalnormal.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The weak malnormality assertion for the edge group in CMMW Theorem 3.2, with its published hypotheses discharged for arbitrary Artin matrices.

theorem OAI.HarmonicArtin.ParabolicIntersections.visual_edge_weaklyMalnormal line 18
Source documentation
The edge group of every visual splitting of an irreducible Artin group is weakly malnormal.
```
theorem visual_edge_weaklyMalnormal (hIrred : IsIrreducible M) :
    WeaklyMalnormal (artinParabolic M (Y∩Z)) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal, OAI.HarmonicArtin.artinParabolic