OAI/GroupTheory/Kervaire/RibbonProducts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KervaireRibbon.transportLetter line 14
2. def OAI.KervaireRibbon.transportEval line 16
3. lemma OAI.KervaireRibbon.dartEval_path line 19
4. lemma OAI.KervaireRibbon.OuterRibbon.value_formula line 40
5. lemma OAI.KervaireRibbon.transportEval_map_gauge line 56
6. lemma OAI.KervaireRibbon.transportEval_append line 70
7. def OAI.KervaireRibbon.OuterRibbon.mul line 76

   Source documentation

   Gluing the marked outside disks along a zero-sign corner concatenates their words. The second potential is gauged to agree at the glued marker.

   def OuterRibbon.mul {ρ : Perm I} {a : I → A} {s : I → ℤ}
       {o : D} {p : E} {l : List D} {m : List E}
       (r : OuterRibbon (V := V) ρ a s o l) (q : OuterRibbon (V := W) ρ a s p m) :
   …

   Mentions: OAI.KervaireRibbon.OuterRibbon

8. lemma OAI.KervaireRibbon.OuterRibbon.value_mul line 182