OAI/NumberTheory/Ostmann/Arithmetic/PrimeMixedLineFamiliesBasic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.CommonZero line 9
  2. def OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.Solutions line 12
  3. def OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.minor line 14
  4. def OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.AllZero line 16
  5. def OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.AllMinorsZero line 18
  6. theorem OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.rank_two_empty line 20
  7. theorem OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.zero_external_coefficient_empty line 26
  8. theorem OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.all_zero_common line 33
  9. theorem OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.commonZero_iff_row line 38
  10. def OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.mixedLineEquiv line 49
  11. def OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.allZeroEquiv line 54
  12. theorem OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.solutions_nonempty_iff line 60
  13. theorem OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.card_rank_one line 84
  14. theorem OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.card_all_zero line 89
  15. theorem OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.card_rank_two line 93
  16. theorem OAI.Ostmann.Arithmetic.PrimeMixedLineFamilies.card_zero_external_coefficient line 98