ParabolicProductProper.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

In irreducible type, two proper standard parabolics never multiply to the whole Coxeter or Artin group. This detects proper parabolic subtrees.

lemma OAI.HarmonicArtin.ParabolicIntersections.coxeter_simple_not_parabolic line 15
theorem OAI.HarmonicArtin.ParabolicIntersections.coxeter_parabolic_product_proper line 26
Source documentation
A noncommutation path supplies an explicit missing double coset.
```
theorem coxeter_parabolic_product_proper (hIrred : IsIrreducible M)
    (X C : Set S) (hX : X≠Set.univ) (hC : C≠Set.univ) :
    ∃ w : M.Group, ∀ a∈parabolic cs X, ∀ b∈parabolic cs C, w≠a*b := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible
theorem OAI.HarmonicArtin.ParabolicIntersections.artin_parabolic_product_proper line 67
Source documentation
The same proper-product statement for the actual Artin presentation.
```
theorem artin_parabolic_product_proper (hIrred : IsIrreducible M)
    (X C : Set S) (hX : X≠Set.univ) (hC : C≠Set.univ) :
    ∃ g : Artin M, ∀ a∈artinParabolic M X, ∀ b∈artinParabolic M C, g≠a*b := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic