OAI/Topology/ArtinGroups/Model.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.alternating line 11

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:13 (same declaration text), ComparatorChallenges/HarmonicArtin.lean:11 (same declaration text).

  2. def OAI.HarmonicArtin.braidRelators line 15

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:17 (same declaration text), ComparatorChallenges/HarmonicArtin.lean:15 (same declaration text).

  3. abbrev OAI.HarmonicArtin.Artin line 20

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:22 (same declaration text), ComparatorChallenges/HarmonicArtin.lean:20 (same declaration text).

  4. def OAI.HarmonicArtin.generator line 22

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:24 (same declaration text), ComparatorChallenges/HarmonicArtin.lean:22 (same declaration text).

  5. def OAI.HarmonicArtin.coxeterParabolic line 24

    Also declared: ComparatorChallenges/HarmonicArtin.lean:24 (same declaration text).

  6. def OAI.HarmonicArtin.IsSpherical line 27

    Also declared: ComparatorChallenges/HarmonicArtin.lean:27 (same declaration text).

  7. abbrev OAI.HarmonicArtin.SphericalType line 30

    Also declared: ComparatorChallenges/HarmonicArtin.lean:30 (same declaration text).

  8. abbrev OAI.HarmonicArtin.LiftedCell line 32

    Also declared: ComparatorChallenges/HarmonicArtin.lean:32 (same declaration text).

  9. def OAI.HarmonicArtin.wordArtin line 34

    Also declared: ComparatorChallenges/HarmonicArtin.lean:34 (same declaration text).

  10. def OAI.HarmonicArtin.wordCoxeter line 37

    Also declared: ComparatorChallenges/HarmonicArtin.lean:37 (same declaration text).

  11. def OAI.HarmonicArtin.LiftedFace line 40

    Also declared: ComparatorChallenges/HarmonicArtin.lean:40 (same declaration text).

  12. instance OAI.HarmonicArtin.(instance at line 49) line 49
  13. def OAI.HarmonicArtin.SalvettiCover line 54

    Also declared: ComparatorChallenges/HarmonicArtin.lean:54 (same declaration text).