OAI/Algebra/FiniteTensor/BoxCoefficients.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Squarefree box coefficients and finite tensor primitives.

  1. abbrev OAI.PD4Tensor.Spreading.Box line 15
  2. def OAI.PD4Tensor.Spreading.boxExponent line 17
  3. theorem OAI.PD4Tensor.Spreading.boxExponent_apply line 20
  4. theorem OAI.PD4Tensor.Spreading.boxExponent_injective line 23
  5. theorem OAI.PD4Tensor.Spreading.squareIdeal_as_monomials line 29
  6. theorem OAI.PD4Tensor.Spreading.squareIdeal_coeff_iff line 42
  7. def OAI.PD4Tensor.Spreading.boxCoeff line 67
  8. theorem OAI.PD4Tensor.Spreading.boxCoeff_mk line 71
  9. theorem OAI.PD4Tensor.Spreading.parameters_ext line 74
  10. theorem OAI.PD4Tensor.Spreading.boxCoeff_mapParameters line 86
  11. theorem OAI.PD4Tensor.Spreading.mapParameters_injective line 92
  12. def OAI.PD4Tensor.Spreading.boxMonomial line 102
  13. theorem OAI.PD4Tensor.Spreading.boxCoeff_boxMonomial line 105
  14. theorem OAI.PD4Tensor.Spreading.sum_boxMonomial line 111
  15. def OAI.PD4Tensor.Spreading.boxSeries line 119
  16. theorem OAI.PD4Tensor.Spreading.coeff_boxSeries line 122
  17. theorem OAI.PD4Tensor.Spreading.sum_boxSeries line 126
  18. theorem OAI.PD4Tensor.Spreading.map_boxMonomial line 145
  19. theorem OAI.PD4Tensor.Spreading.sub_constant_parameters_mem line 151
  20. theorem OAI.PD4Tensor.Spreading.augmentation_eq_zero_of_mem line 169
  21. theorem OAI.PD4Tensor.Spreading.mem_parameterIdeal_iff line 177
  22. theorem OAI.PD4Tensor.Spreading.mapParameters_mem_iff line 184
  23. def OAI.PD4Tensor.Spreading.liftParameterSeries line 192
  24. theorem OAI.PD4Tensor.Spreading.map_liftParameterSeries line 199
  25. abbrev OAI.PD4Tensor.Spreading.Triple line 224
  26. structure OAI.PD4Tensor.Spreading.TensorPrimitives line 229
  27. theorem OAI.PD4Tensor.Spreading.exists_tensorPrimitives line 243