OAI/Combinatorics/PolynomialVacuum/Algebra/NodeFactors.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumInterpolation.mergeVariable_C line 8
  2. theorem OAI.PolynomialVacuumInterpolation.mergeVariable_X line 10
  3. theorem OAI.PolynomialVacuumInterpolation.nodeFactor_dvd_sub_merge line 14
  4. theorem OAI.PolynomialVacuumInterpolation.mergeVariable_nodeFactor line 34
  5. theorem OAI.PolynomialVacuumInterpolation.nodeFactor_dvd_iff line 39
  6. theorem OAI.PolynomialVacuumInterpolation.nodeFactor_ne_zero line 46
  7. theorem OAI.PolynomialVacuumInterpolation.nodeFactor_prime line 50
  8. theorem OAI.PolynomialVacuumInterpolation.nodeFactor_not_dvd line 60
  9. theorem OAI.PolynomialVacuumInterpolation.nodeFactor_isRelPrime line 68