OAI/Algebra/FiniteTensor/ScalarModels.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Squarefree scalar tensor models, primitives and complementary dimensions.

  1. def OAI.PD4Tensor.Spreading.squareIdeal line 14
  2. abbrev OAI.PD4Tensor.Spreading.Parameters line 17
  3. def OAI.PD4Tensor.Spreading.parameter line 19
  4. def OAI.PD4Tensor.Spreading.augmentation line 22
  5. def OAI.PD4Tensor.Spreading.parameterIdeal line 32
  6. theorem OAI.PD4Tensor.Spreading.parameter_sq line 34
  7. theorem OAI.PD4Tensor.Spreading.augmentation_parameter line 39
  8. theorem OAI.PD4Tensor.Spreading.augmentation_algebraMap line 43
  9. theorem OAI.PD4Tensor.Spreading.parameterIdeal_le_nilradical line 48
  10. theorem OAI.PD4Tensor.Spreading.hasSubst_parameters line 53
  11. def OAI.PD4Tensor.Spreading.mapParameters line 63
  12. theorem OAI.PD4Tensor.Spreading.mapParameters_parameter line 75
  13. theorem OAI.PD4Tensor.Spreading.mapParameters_algebraMap line 81
  14. theorem OAI.PD4Tensor.Spreading.augmentation_mapParameters line 88
  15. theorem OAI.PD4Tensor.Spreading.mapParameters_mem line 102
  16. def OAI.PD4Tensor.Spreading.potential line 121
  17. def OAI.PD4Tensor.Spreading.perturbation line 124
  18. def OAI.PD4Tensor.Spreading.deformed line 128
  19. def OAI.PD4Tensor.Spreading.tangent line 135
  20. structure OAI.PD4Tensor.Spreading.TensorModel line 145
  21. theorem OAI.PD4Tensor.Spreading.map_potential line 178
  22. theorem OAI.PD4Tensor.Spreading.map_perturbation line 184
  23. theorem OAI.PD4Tensor.Spreading.map_coefficient_extension line 190
  24. theorem OAI.PD4Tensor.Spreading.map_deformed line 198
  25. theorem OAI.PD4Tensor.Spreading.map_tangent line 207
  26. def OAI.PD4Tensor.Spreading.TensorModel.map line 220
  27. theorem OAI.PD4Tensor.joinedMatrix_complementary line 269