ReducedPositiveExtension.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Cancelling common atoms in a spherical common left extension.

theorem OAI.HarmonicArtin.ParabolicIntersections.spherical_reduced_positive_extension line 16
Source documentation
The finite-type fraction theorem gives a common positive extension whose two positive factors have no common left atom. Choosing the least sum of positive lengths proves termination of the cancellation process.
```
theorem spherical_reduced_positive_extension (Y : Set S) (hY : IsSpherical M Y)
    (a b : Artin (restrictedMatrix M Y)) :
    ∃ p q : PositiveArtin (restrictedMatrix M Y),
      positiveToArtin _ p*a=positiveToArtin _ q*b ∧
      ∀ s : Y, ¬ (PositivePrefix _ (positiveGenerator _ s) p ∧
        PositivePrefix _ (positiveGenerator _ s) q) := by
…
```
Mentions: OAI.HarmonicArtin.IsSpherical, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.PositiveArtin, OAI.HarmonicArtin.positiveToArtin, OAI.HarmonicArtin.PositivePrefix, OAI.HarmonicArtin.positiveGenerator