OAI/Algebra/FiniteTensor/AdicSystems.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Quadratic remainders, adic contraction and Tougeron corrections.

  1. def OAI.PD4Tensor.Spreading.mvShift line 16
  2. def OAI.PD4Tensor.Spreading.mvLinearPart line 19
  3. def OAI.PD4Tensor.Spreading.mvRemainder line 22
  4. theorem OAI.PD4Tensor.Spreading.mvLinearPart_mul_X line 25
  5. theorem OAI.PD4Tensor.Spreading.mvRemainder_mul_X line 40
  6. theorem OAI.PD4Tensor.Spreading.mvRemainder_mem line 46
  7. theorem OAI.PD4Tensor.Spreading.mv_polynomial_quadratic_remainder line 75
  8. theorem OAI.PD4Tensor.Spreading.mv_eval_quadratic_remainder line 96
  9. theorem OAI.PD4Tensor.Spreading.mv_eval_sub_mem line 130
  10. theorem OAI.PD4Tensor.Spreading.mv_quadratic_sub_mem line 145
  11. theorem OAI.PD4Tensor.Spreading.adic_quadratic_system line 177
  12. theorem OAI.PD4Tensor.Spreading.adic_contractive_system line 269
  13. theorem OAI.PD4Tensor.Spreading.mv_quadratic_mixed_sub_mem line 354
  14. theorem OAI.PD4Tensor.Spreading.mulVec_mem_ideal line 384
  15. theorem OAI.PD4Tensor.Spreading.mulVec_sub_mem_ideal line 391
  16. theorem OAI.PD4Tensor.Spreading.mv_tougeron_correction line 398
  17. theorem OAI.PD4Tensor.Spreading.det_sub_mem_ideal line 465
  18. theorem OAI.PD4Tensor.Spreading.corrected_jacobian_factor line 476
  19. theorem OAI.PD4Tensor.Spreading.mv_tougeron_nondegenerate line 497