OAI/RingTheory/DirectFiniteness/FiniteParameters.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.FiniteGeometry.sourceQ line 9
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourceQ_ge line 11
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourceQ_large line 14
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourceQ_pos line 17
5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.exponent_comparison line 19
6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourceQ_density line 23
7. lemma OAI.KaplanskyCounterexample.FiniteGeometry.source_prime_exists line 27
8. def OAI.KaplanskyCounterexample.FiniteGeometry.sourcePrime line 40
9. def OAI.KaplanskyCounterexample.FiniteGeometry.sourceD line 42
10. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourcePrime_prime line 44
11. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourcePrime_le line 45
12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourceD_divisible line 47
13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourceD_bounds line 49
14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourceD_q_dvd line 63
15. lemma OAI.KaplanskyCounterexample.FiniteGeometry.sourceD_log line 66