OAI/Topology/ArtinGroups/ParabolicIntersections/FoldingGcd.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Discharge of the published common-left-atom folding input.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.expanded_braid_prefix line 19
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.folding_gcd_input line 44

    Source documentation

    Castella's common-atom consequence, now proved for the particular color folding rather than supplied as a hypothesis.

    theorem folding_gcd_input : PublishedFoldingGcd M Y hY where
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedFoldingGcd