OAI/Combinatorics/PolynomialVacuum/Algebra/LagrangeClearing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.nodeDenominator line 9
  2. def OAI.PolynomialVacuumAlgebra.allNodeDenominators line 11
  3. def OAI.PolynomialVacuumAlgebra.exceptNodeDenominator line 13
  4. def OAI.PolynomialVacuumAlgebra.nodeNumerator line 15
  5. theorem OAI.PolynomialVacuumAlgebra.nodeDenominator_ne_zero line 18
  6. theorem OAI.PolynomialVacuumAlgebra.allNodeDenominators_ne_zero line 24
  7. theorem OAI.PolynomialVacuumAlgebra.allNodeDenominators_factor line 28
  8. theorem OAI.PolynomialVacuumAlgebra.nodeNumerator_self line 32
  9. theorem OAI.PolynomialVacuumAlgebra.nodeNumerator_other line 36
  10. theorem OAI.PolynomialVacuumAlgebra.nodeNumerator_natDegree line 42
  11. theorem OAI.PolynomialVacuumAlgebra.canonicalInterpolant_cleared line 53