OAI/Algebra/FiniteTensor/RelativeKoszul.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Relative Koszul operators and specialization of deformed separated forms.

  1. def OAI.PD4Tensor.FiniteCoordinates.relativeD line 19
  2. theorem OAI.PD4Tensor.FiniteCoordinates.relativeD_eq line 23
  3. def OAI.PD4Tensor.FiniteCoordinates.relativeKoszul line 31
  4. theorem OAI.PD4Tensor.FiniteCoordinates.relativeKoszul_eq line 35
  5. theorem OAI.PD4Tensor.FiniteCoordinates.scalar_parameter_smul line 42
  6. theorem OAI.PD4Tensor.FiniteCoordinates.relativeKoszul_add line 47
  7. theorem OAI.PD4Tensor.FiniteCoordinates.relativeKoszul_zero line 54
  8. theorem OAI.PD4Tensor.FiniteCoordinates.relativeKoszul_smul line 60
  9. theorem OAI.PD4Tensor.FiniteCoordinates.relativeKoszul_sum line 68
  10. theorem OAI.PD4Tensor.FiniteCoordinates.relativeKoszul_coefficientMap line 77
  11. theorem OAI.PD4Tensor.FiniteCoordinates.relativeKoszul_deformation line 110
  12. def OAI.PD4Tensor.TruncatedForms.sigmaExtendedForms line 142
  13. theorem OAI.PD4Tensor.TruncatedForms.relativeKoszul_sigmaExtended line 150
  14. theorem OAI.PD4Tensor.TruncatedForms.sigmaExtendedForms_specialization line 193
  15. theorem OAI.PD4Tensor.FiniteCoordinates.chartNormal_specialization line 284
  16. theorem OAI.PD4Tensor.parameterCharP line 312
  17. theorem OAI.PD4Tensor.FiniteCoordinates.scalar_parameter_mul line 327