OAI/Topology/ArtinGroups/ParabolicIntersections/PositiveTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Relabeling positive Artin monoids and finite-type cancellation.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.altList_map line 10
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveMap_relations line 20
  3. def OAI.HarmonicArtin.ParabolicIntersections.positiveMap line 33
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveMap_generator line 36
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveMap_word line 39
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveMap_prefix line 43
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.finite_positive_cancel_left line 50

    Source documentation

    Cancellation in a finite Coxeter type, without an artificial subtype of generators in the statement.

    theorem finite_positive_cancel_left [Fintype S] [LinearOrder S] [Finite M.Group]
    (a b c : PositiveArtin M) (h : a*b=a*c) : b=c := by
…

    Mentions: OAI.HarmonicArtin.PositiveArtin