OAI/RingTheory/DirectFiniteness/BalanceCoarsening.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Cycles map under a coarsening of the orbit partition.

   def cycleMap {p q : Perm α} (h : ∀ {x y}, p.SameCycle x y → q.SameCycle x y) :
       Cycles p → Cycles q := Quotient.map id (fun _ _ hxy => h hxy)
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Cycles

2. lemma OAI.KaplanskyCounterexample.Planar.cycleMap_class line 20
3. lemma OAI.KaplanskyCounterexample.Planar.sum_cycle_coarsen line 23
4. lemma OAI.KaplanskyCounterexample.Planar.sum_cycle_coarsen_zero line 34
5. lemma OAI.KaplanskyCounterexample.Planar.sum_cycle_coarsen_exception line 41
6. structure OAI.KaplanskyCounterexample.Planar.WeakBalanced line 64

   Source documentation

   The same balances, allowing temporary zero edges during cancellation.

   structure WeakBalanced (R : Ribbon α) (Inc : V → F → Prop)
       (ι : V → F → (A →+ B)) where
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon

7. def OAI.KaplanskyCounterexample.Planar.Balanced.weak line 81
8. def OAI.KaplanskyCounterexample.Planar.WeakBalanced.strong line 93
9. def OAI.KaplanskyCounterexample.Planar.WeakBalanced.coarsen line 107