OAI/RingTheory/DirectFiniteness/BalanceDetachment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.Planar.label_sameCycle line 15
2. lemma OAI.KaplanskyCounterexample.Planar.label_unplug line 19
3. lemma OAI.KaplanskyCounterexample.Planar.sameCycle_unplug_iff_of_ne line 23
4. lemma OAI.KaplanskyCounterexample.Planar.cycleSet_unplug line 30
5. lemma OAI.KaplanskyCounterexample.Planar.sum_erase_of_zero line 46
6. lemma OAI.KaplanskyCounterexample.Planar.sum_cycle_unplug line 54
7. lemma OAI.KaplanskyCounterexample.Planar.WeakBalanced.exists_exception_nonzero line 63
8. def OAI.KaplanskyCounterexample.Planar.WeakBalanced.detach line 70

   Source documentation

   A zero-weight edge can be detached without changing any nonzero balance.

   def WeakBalanced.detach (D : WeakBalanced R Inc ι) (a : α) (ha : D.weight a = 0) :
       WeakBalanced (R.detach a) Inc ι := by
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.WeakBalanced