OAI/NumberTheory/Ostmann/Arithmetic/PrimeLineFamiliesBasic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.PrimeLineFamilies.CommonZero line 9
  2. def OAI.Ostmann.Arithmetic.PrimeLineFamilies.Solutions line 12
  3. def OAI.Ostmann.Arithmetic.PrimeLineFamilies.minor line 14
  4. def OAI.Ostmann.Arithmetic.PrimeLineFamilies.AllZero line 16
  5. def OAI.Ostmann.Arithmetic.PrimeLineFamilies.AllMinorsZero line 18
  6. theorem OAI.Ostmann.Arithmetic.PrimeLineFamilies.rank_two_empty line 20
  7. theorem OAI.Ostmann.Arithmetic.PrimeLineFamilies.single_coefficient_empty line 26
  8. theorem OAI.Ostmann.Arithmetic.PrimeLineFamilies.all_zero_common line 36
  9. theorem OAI.Ostmann.Arithmetic.PrimeLineFamilies.commonZero_iff_row line 41
  10. def OAI.Ostmann.Arithmetic.PrimeLineFamilies.unitLineEquiv line 52
  11. def OAI.Ostmann.Arithmetic.PrimeLineFamilies.allZeroEquiv line 57
  12. theorem OAI.Ostmann.Arithmetic.PrimeLineFamilies.solutions_nonempty_iff line 64
  13. theorem OAI.Ostmann.Arithmetic.PrimeLineFamilies.card_rank_one line 92
  14. theorem OAI.Ostmann.Arithmetic.PrimeLineFamilies.card_all_zero line 97
  15. theorem OAI.Ostmann.Arithmetic.PrimeLineFamilies.card_rank_two line 101
  16. theorem OAI.Ostmann.Arithmetic.PrimeLineFamilies.card_single_coefficient line 106