OAI/GroupTheory/Kervaire/Realization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KervaireRibbon.OuterRibbon.one line 13
  2. lemma OAI.KervaireRibbon.OuterRibbon.value_one line 33
  3. def OAI.KervaireRibbon.Realized line 39

    Source documentation

    A word is realized by a finite genus-zero relator ribbon. The dart and vertex sets range over ordinary finite types; the coefficient group has arbitrary universe.

    def Realized (ρ : Perm I) (a : I → A) (s : I → ℤ) (w : FreeProd A) : Prop :=
…

    Mentions: OAI.KervaireRibbon.FreeProd

  4. lemma OAI.KervaireRibbon.Realized.one line 43
  5. lemma OAI.KervaireRibbon.Realized.mul line 47
  6. lemma OAI.KervaireRibbon.Realized.inv line 54
  7. lemma OAI.KervaireRibbon.Realized.conjCoefficient line 59
  8. lemma OAI.KervaireRibbon.Realized.conjLetter line 64
  9. def OAI.KervaireRibbon.realizedSubgroup line 71
  10. lemma OAI.KervaireRibbon.Realized.conjZpow line 77
  11. lemma OAI.KervaireRibbon.Realized.conj line 93
  12. instance OAI.KervaireRibbon.realizedSubgroup_normal line 103
  13. lemma OAI.KervaireRibbon.Realized.coefficient_eq_one line 107