OAI/GroupTheory/Kervaire/Inversion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KervaireRibbon.perm_apply_inverse line 14
2. lemma OAI.KervaireRibbon.perm_inverse_apply line 17
3. lemma OAI.KervaireRibbon.cycles_inv line 21
4. lemma OAI.KervaireRibbon.numCycles_inverse line 25
5. lemma OAI.KervaireRibbon.planar_inverse line 29
6. lemma OAI.KervaireRibbon.circle_inverse line 44
7. def OAI.KervaireRibbon.OuterRibbon.inv line 57

   Source documentation

   Reflection reverses every vertex, negates the traversal signs, and exchanges both sides of each band potential.

   def OuterRibbon.inv {ρ : Perm I} {a : I → A} {s : I → ℤ} {o : D} {l : List D}
       (r : OuterRibbon (V := V) ρ a s o l) : OuterRibbon (V := V) ρ a s o l.reverse := by
   …

   Mentions: OAI.KervaireRibbon.OuterRibbon

8. lemma OAI.KervaireRibbon.OuterRibbon.value_inv line 106