OAI/NumberTheory/Ostmann/Arithmetic/ClearedCoefficientFlags.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.leftCoefficient line 12
  2. def OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.rightCoefficient line 13
  3. def OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.commonDenominator line 14
  4. def OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.minor line 16
  5. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.coefficients_cleared line 19
  6. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.linear_zero_iff line 35
  7. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.row_nonzero_iff line 44
  8. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.minor_cleared line 53
  9. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.minor_zero_iff line 65
  10. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.coefficient_degrees line 74
  11. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.minor_degree line 84
  12. def OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.PolynomialAbove line 96
  13. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.polynomialAbove_mul line 99
  14. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.fraction_above line 107
  15. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.coefficients_above line 113
  16. theorem OAI.Ostmann.Arithmetic.ClearedCoefficientFlags.minor_above line 122