OAI/Algebra/FiniteTensor/SquarefreeParameters.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Squarefree parameter algebras, selectors and formal gradient base change.

  1. def OAI.PD4Tensor.squareIdeal line 17
  2. abbrev OAI.PD4Tensor.T line 20
  3. def OAI.PD4Tensor.t line 22
  4. def OAI.PD4Tensor.augmentation line 24
  5. def OAI.PD4Tensor.parameterIdeal line 34
  6. theorem OAI.PD4Tensor.t_sq line 42
  7. theorem OAI.PD4Tensor.parameterIdeal_le_nilradical line 48
  8. theorem OAI.PD4Tensor.squareIdeal_as_monomials line 53
  9. theorem OAI.PD4Tensor.squarefree_monomial_ne_zero line 67
  10. theorem OAI.PD4Tensor.triple_ne_zero line 79
  11. theorem OAI.PD4Tensor.triple_mul_unit_ne_zero line 94
  12. theorem OAI.PD4Tensor.augmentation_t line 101
  13. theorem OAI.PD4Tensor.augmentation_algebraMap line 104
  14. def OAI.PD4Tensor.augmentationAlg line 109
  15. theorem OAI.PD4Tensor.sub_constant_mem line 113
  16. theorem OAI.PD4Tensor.isUnit_of_augmentation_ne_zero line 133
  17. def OAI.PD4Tensor.threeParameters line 147
  18. theorem OAI.PD4Tensor.threeParameters_selected line 150
  19. theorem OAI.PD4Tensor.threeParameters_other line 153
  20. theorem OAI.PD4Tensor.threeParameters_sq line 156
  21. theorem OAI.PD4Tensor.augmentation_threeParameters line 163
  22. def OAI.PD4Tensor.parameterSelector line 178
  23. theorem OAI.PD4Tensor.parameterSelector_t line 188
  24. theorem OAI.PD4Tensor.augmentation_parameterSelector line 193
  25. theorem OAI.PD4Tensor.augmentation_zero_of_mem line 203
  26. theorem OAI.PD4Tensor.map_formal_pderiv line 219
  27. theorem OAI.PD4Tensor.map_formal_gradient line 228
  28. def OAI.PD4Tensor.activeExtension line 253
  29. theorem OAI.PD4Tensor.activeExtension_selected line 256
  30. theorem OAI.PD4Tensor.activeExtension_other line 266
  31. theorem OAI.PD4Tensor.sum_activeExtension line 276
  32. theorem OAI.PD4Tensor.embedding_preimage line 293