OAI/Combinatorics/PolynomialVacuum/Algebra/CupDivisibility.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumAlgebra.cupFactor line 8
  2. theorem OAI.PolynomialVacuumAlgebra.substitution_factor_dvd line 10
  3. theorem OAI.PolynomialVacuumAlgebra.cupFactor_dvd_of_specialize_zero line 28
  4. theorem OAI.PolynomialVacuumAlgebra.X_sub_scaled_X_ne_zero line 32
  5. theorem OAI.PolynomialVacuumAlgebra.cupFactor_ne_zero line 38
  6. theorem OAI.PolynomialVacuumAlgebra.cupSpecialize_cupFactor_ne_zero line 41
  7. theorem OAI.PolynomialVacuumAlgebra.cupProduct_dvd line 60
  8. def OAI.PolynomialVacuumAlgebra.cupPairs line 87
  9. def OAI.PolynomialVacuumAlgebra.cupVandermonde line 89
  10. theorem OAI.PolynomialVacuumAlgebra.mem_cupPairs line 92
  11. theorem OAI.PolynomialVacuumAlgebra.cupVandermonde_ne_zero line 96
  12. theorem OAI.PolynomialVacuumAlgebra.cupVandermonde_dvd line 101