OAI/RingTheory/DirectFiniteness/PartitionMerging.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyCounterexample.Planar.mergeClass line 16

    Source documentation

    Identify two classes of a partition, by redirecting the second to the first.

    def mergeClass (s : Setoid α) (a b x : α) : Quotient s :=
…
  2. def OAI.KaplanskyCounterexample.Planar.joinPair line 19
  3. lemma OAI.KaplanskyCounterexample.Planar.le_joinPair line 21
  4. lemma OAI.KaplanskyCounterexample.Planar.joinPair_related line 26
  5. lemma OAI.KaplanskyCounterexample.Planar.joinPair_eq_of_related line 30
  6. lemma OAI.KaplanskyCounterexample.Planar.joinPair_le line 42
  7. def OAI.KaplanskyCounterexample.Planar.joinPairEquiv line 58

    Source documentation

    When the two old classes are distinct, joining them removes exactly one.

    def joinPairEquiv (s : Setoid α) (a b : α) (hab : ¬ s.r a b) :
    Quotient (joinPair s a b) ≃ {c : Quotient s // c ≠ Quotient.mk s b} where
…

    Mentions: OAI.KaplanskyCounterexample.Planar.joinPair

  8. lemma OAI.KaplanskyCounterexample.Planar.joinPair_card line 82
  9. lemma OAI.KaplanskyCounterexample.Planar.setoid_swap_related line 90
  10. lemma OAI.KaplanskyCounterexample.Planar.setoid_sameCycle_of_step line 100
  11. def OAI.KaplanskyCounterexample.Planar.edgePartition line 111

    Source documentation

    Connected components of a graph presented as a list of edges.

    def edgePartition : List (α × α) → Setoid α
  | [] => ⊥
  | (a, b) :: l => joinPair (edgePartition l) a b

    Mentions: OAI.KaplanskyCounterexample.Planar.joinPair

  12. lemma OAI.KaplanskyCounterexample.Planar.edgePartition_le line 115
  13. lemma OAI.KaplanskyCounterexample.Planar.edgePartition_pair line 123
  14. lemma OAI.KaplanskyCounterexample.Planar.edgePartition_prod line 132
  15. lemma OAI.KaplanskyCounterexample.Planar.transposition_euler_bound line 141