OAI/RingTheory/DirectFiniteness/TradeFamily.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.LiveLine line 14
  2. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.LiveIndex line 15
  3. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.NewIndex line 16
  4. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.TradeIndex line 17
  5. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.tradeLine line 19
  6. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.tradeLabel line 23
  7. instance OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.(instance at line 27) line 27
  8. instance OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.(instance at line 28) line 28
  9. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.live_through line 30
  10. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.live_full line 35
  11. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.tradeLine_full line 40
  12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.tradeLine_avoid line 45
  13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.same_label_eq line 51
  14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.live_step line 77
  15. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.tradeLine_step_mem line 83
  16. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.removed_iff line 96