OAI/Combinatorics/PerfectMatching/Model.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MatchingEntropy.LooplessGraph line 8

    Distinct definitions of this name: ComparatorChallenges/BinaryMatching.lean:9 (same declaration text), ComparatorChallenges/MatchingEntropy.lean:15 (different declaration text), ComparatorChallenges/SingletonLoopMatching.lean:8 (same declaration text). Qualify references as OAI.MatchingEntropy.LooplessGraph@path.

  2. def OAI.MatchingEntropy.LooplessGraph.Incident line 14

    Distinct definitions of this name: ComparatorChallenges/BinaryMatching.lean:17 (same declaration text), ComparatorChallenges/MatchingEntropy.lean:24 (same statement text; different proof or body), ComparatorChallenges/SingletonLoopMatching.lean:14 (same declaration text). Qualify references as OAI.MatchingEntropy.LooplessGraph.Incident@path.

  3. def OAI.MatchingEntropy.LooplessGraph.IsPerfectMatching line 16

    Distinct definitions of this name: ComparatorChallenges/BinaryMatching.lean:19 (same declaration text), ComparatorChallenges/MatchingEntropy.lean:27 (same statement text; different proof or body). Qualify references as OAI.MatchingEntropy.LooplessGraph.IsPerfectMatching@path.

  4. abbrev OAI.MatchingEntropy.LooplessGraph.Matching line 18

    Also declared: ComparatorChallenges/BinaryMatching.lean:21 (same declaration text), ComparatorChallenges/MatchingEntropy.lean:30 (same declaration text).

  5. instance OAI.MatchingEntropy.LooplessGraph.matchingFintype line 19

    Distinct definitions of this name: ComparatorChallenges/BinaryMatching.lean:22 (same declaration text), ComparatorChallenges/MatchingEntropy.lean:32 (different declaration text). Qualify references as OAI.MatchingEntropy.LooplessGraph.matchingFintype@path.

  6. abbrev OAI.BinaryMatching.Pair line 25

    Also declared: ComparatorChallenges/BinaryMatching.lean:31 (same declaration text), ComparatorChallenges/SingletonLoopMatching.lean:20 (same declaration text).

  7. def OAI.BinaryMatching.completeGraph line 26

    Also declared: ComparatorChallenges/BinaryMatching.lean:32 (same declaration text), ComparatorChallenges/SingletonLoopMatching.lean:21 (same declaration text).

  8. structure OAI.BinaryMatching.Record line 31

    Also declared: ComparatorChallenges/BinaryMatching.lean:37 (same declaration text), ComparatorChallenges/SingletonLoopMatching.lean:26 (same declaration text).

  9. structure OAI.BinaryMatching.Input line 37

    Also declared: ComparatorChallenges/BinaryMatching.lean:43 (same declaration text), ComparatorChallenges/SingletonLoopMatching.lean:32 (same declaration text).

  10. def OAI.BinaryMatching.multiplicity line 43

    Also declared: ComparatorChallenges/BinaryMatching.lean:49 (same declaration text), ComparatorChallenges/SingletonLoopMatching.lean:38 (same declaration text).

  11. def OAI.BinaryMatching.count line 48

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

  12. def OAI.BinaryMatching.encodeNat line 51

    Also declared: ComparatorChallenges/BinaryMatching.lean:57 (same declaration text), ComparatorChallenges/SingletonLoopMatching.lean:44 (same declaration text).

  13. def OAI.BinaryMatching.encodeRecord line 54

    Also declared: ComparatorChallenges/BinaryMatching.lean:60 (same declaration text), ComparatorChallenges/SingletonLoopMatching.lean:47 (same declaration text).

  14. def OAI.BinaryMatching.encodeInput line 57

    Also declared: ComparatorChallenges/BinaryMatching.lean:63 (same declaration text), ComparatorChallenges/SingletonLoopMatching.lean:50 (same declaration text).