OAI/NumberTheory/Ostmann/Arithmetic/PrimeLines.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.PrimeLines.mixedLineEquiv line 11
2. def OAI.Ostmann.Arithmetic.PrimeLines.unitLineEquiv line 24
3. theorem OAI.Ostmann.Arithmetic.PrimeLines.rank_two_impossible line 40
4. theorem OAI.Ostmann.Arithmetic.PrimeLines.no_unit_solution_of_zero_coefficient line 46
5. theorem OAI.Ostmann.Arithmetic.PrimeLines.card_mixed_line line 51
6. theorem OAI.Ostmann.Arithmetic.PrimeLines.card_unit_line line 55
7. theorem OAI.Ostmann.Arithmetic.PrimeLines.prime_mixed_probability line 59
8. theorem OAI.Ostmann.Arithmetic.PrimeLines.prime_unit_probability line 69