RowReducedChart.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of row charts and one-root charts

Removing one coordinate from the row time space gives precisely the transversal of the existing one-root chart. The parameterizations agree pointwise, so their disintegrations refer to the same actual root leaves.

def OAI.DukePrimeDegree.rowReducedHomeomorph line 21
theorem OAI.DukePrimeDegree.row_one_root_parametrization line 53
Source documentation
The single-root and simultaneous-row parameterizations agree, with the selected real parameter occupying the last factor.
```
theorem row_one_root_parametrization {n : ℕ} {i j : Fin n} (hij : i ≠ j) (k : Fin n)
    (s : RowRootSlice i k) (w : RowRemainingTime i j) (t : ℝ) :
    rootQuotientParametrization hij ((rowReducedHomeomorph hij k).symm (s, w), t) =
      rowQuotientParametrization i k (s, w.val + t • rowUnit hij) := by
…
```
Mentions: OAI.DukePrimeDegree.RowRootSlice, OAI.DukePrimeDegree.RowRemainingTime, OAI.DukePrimeDegree.rowReducedHomeomorph, OAI.DukePrimeDegree.rowQuotientParametrization, OAI.DukePrimeDegree.rowUnit