ParabolicMinimumStep.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The Coxeter coset step used in the standard-parabolic retraction.

theorem OAI.HarmonicArtin.ParabolicIntersections.exists_parabolic_left_descent line 13
Source documentation
A nonminimal element has a left descent in the parabolic colors.
```
theorem exists_parabolic_left_descent (J : Set S) (w : W)
    (hw : ¬ IsParabolicMinimum cs J w) :
    ∃ t ∈ J, cs.length (cs.simple t*w) < cs.length w := by
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.parabolic_minimum_step line 39
Source documentation
Multiplying a minimal left-coset representative by one simple reflection either remains minimal or crosses a wall of the parabolic.
```
theorem parabolic_minimum_step (J : Set S) (v : W)
    (hv : IsParabolicMinimum cs J v) (s : S) :
    IsParabolicMinimum cs J (v*cs.simple s) ∨
      ∃ t ∈ J, v*cs.simple s=cs.simple t*v := by
…
```