OAI/Algebra/AffineCancellation/PolynomialSlice.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ComplexCancellation.DifferentialSlice.constantMap line 9
  2. instance OAI.ComplexCancellation.DifferentialSlice.constantAlgebra line 15
  3. instance OAI.ComplexCancellation.DifferentialSlice.constantTower line 16
  4. def OAI.ComplexCancellation.InvariantClearing.subalgebra line 23
  5. lemma OAI.ComplexCancellation.InvariantClearing.image_mem line 38
  6. abbrev OAI.ComplexCancellation.PolynomialModel.K line 45
  7. abbrev OAI.ComplexCancellation.PolynomialModel.F line 47
  8. def OAI.ComplexCancellation.PolynomialModel.ι line 48
  9. lemma OAI.ComplexCancellation.PolynomialModel.local_slice line 51
  10. def OAI.ComplexCancellation.PolynomialModel.evaluation line 63
  11. lemma OAI.ComplexCancellation.PolynomialModel.evaluation_injective line 65
  12. lemma OAI.ComplexCancellation.PolynomialModel.exists_model line 67
  13. def OAI.ComplexCancellation.PolynomialModel.model line 70
  14. lemma OAI.ComplexCancellation.PolynomialModel.evaluation_model line 89
  15. lemma OAI.ComplexCancellation.PolynomialModel.model_injective line 91
  16. lemma OAI.ComplexCancellation.PolynomialModel.derivative_model line 97
  17. lemma OAI.ComplexCancellation.PolynomialModel.clear_constant line 104
  18. lemma OAI.ComplexCancellation.PolynomialModel.clear_X line 116
  19. lemma OAI.ComplexCancellation.PolynomialModel.clear_polynomial line 128