OAI/Geometry/HyperbolicGroups/Parity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.LetterPresentation.ParityGroup line 15
  2. def OAI.HyperbolicObstruction.LetterPresentation.oddLetter line 16
  3. lemma OAI.HyperbolicObstruction.LetterPresentation.oddLetter_inv line 18
  4. lemma OAI.HyperbolicObstruction.LetterPresentation.oddLetter_mul line 20
  5. lemma OAI.HyperbolicObstruction.LetterPresentation.oddLetter_ne_one line 22
  6. def OAI.HyperbolicObstruction.LetterPresentation.coreParity line 26
  7. lemma OAI.HyperbolicObstruction.LetterPresentation.coreParity_step line 31
  8. lemma OAI.HyperbolicObstruction.LetterPresentation.coreParity_path line 47
  9. lemma OAI.HyperbolicObstruction.LetterPresentation.coreParity_loop line 57
  10. def OAI.HyperbolicObstruction.LetterPresentation.freeParity line 63
  11. lemma OAI.HyperbolicObstruction.LetterPresentation.freeParity_letter line 64
  12. lemma OAI.HyperbolicObstruction.LetterPresentation.relator_parity line 71
  13. def OAI.HyperbolicObstruction.LetterPresentation.parity line 94

    Source documentation

    The source quotient onto Cā‚‚, for every realization including all unmatched rows. No infinitude or asphericity hypothesis is used here.

    def parity : Group n w d ā†’* ParityGroup :=
ā€¦

    Mentions: OAI.HyperbolicObstruction.LetterPresentation.Group, OAI.HyperbolicObstruction.LetterPresentation.ParityGroup

  14. lemma OAI.HyperbolicObstruction.LetterPresentation.parity_letter line 97
  15. lemma OAI.HyperbolicObstruction.LetterPresentation.parity_surjective line 102
  16. lemma OAI.HyperbolicObstruction.LetterPresentation.letter_ne_one line 112
  17. instance OAI.HyperbolicObstruction.LetterPresentation.group_nontrivial line 118