OAI/Topology/ArtinGroups/ParabolicIntersections/FoldingSimpleGcd.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Folding preserves greatest common prefixes of simple elements.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.folded_prefix line 17
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.folded_simple_gcd line 24

    Source documentation

    Greatest common prefixes of simples are preserved by the color folding. The induction removes one complete color at a time.

    theorem folded_simple_gcd (u v g : (R).Group)
    (hgu : PositivePrefix R (P g) (P u)) (hgv : PositivePrefix R (P g) (P v))
    (hg : ∀ e, PositivePrefix R e (P u) → PositivePrefix R e (P v) → PositivePrefix R e (P g)) :
    ∀ e, PositivePrefix N e (Φ (P u)) → PositivePrefix N e (Φ (P v)) →
      PositivePrefix N e (Φ (P g)) := by
…

    Mentions: OAI.HarmonicArtin.PositivePrefix