OAI/RingTheory/DirectFiniteness/SlabEvents.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.ShortCandidate line 16
2. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.SlabEvent line 17
3. instance OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.(instance at line 19) line 19
4. instance OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.(instance at line 20) line 20
5. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.eventDeps line 22
6. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.eventVector line 26
7. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.eventDeps_nonempty line 31
8. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.eventDeps_card line 37
9. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.eventVector_nonzero line 43
10. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.holeEvent_load line 51
11. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.slabLoadBound line 67

    Source documentation

    A convenient literal finite arithmetic load bound, prior to specializing q.

    def slabLoadBound (_F : DirectionFrame Q A R E) (p : ℝ) : ℝ := 100^2*p + ∑ i : Fin 3,
    …

    Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame

12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.event_load_le line 72
13. structure OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.SuccessfulSlabs line 94
14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.exists_eventPlanes line 99
15. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.successful_of_eventPlanes line 118
16. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.exists_successfulSlabs line 132