OAI/RingTheory/DirectFiniteness/TradeDegree.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.KeptAt line 14
2. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.RemovedAt line 15
3. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.NewAt line 16
4. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.LiveAt line 18
5. instance OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.(instance at line 20) line 20
6. instance OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.(instance at line 21) line 21
7. instance OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.(instance at line 22) line 22
8. instance OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.(instance at line 23) line 23
9. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.liveAt_card line 25
10. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.newCoord line 41

    Source documentation

    The second coordinate of a point on a replacement line.

    def newCoord {x : A} (i : F.NewAt O x) : Q :=
    …

11. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.newCoord_spec line 45
12. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.newLabel line 49
13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.newLabel_axis line 53
14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.newLabel_injective line 62
15. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.newLabel_surjective line 73
16. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.newAt_card line 90
17. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.trade_degree line 102