OAI/Algebra/FiniteTensor/FormBaseChange.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Coefficient specialization and base change of form functionals.

  1. theorem OAI.PD4Tensor.FiniteCoordinates.centralD_eq line 18
  2. theorem OAI.PD4Tensor.FiniteCoordinates.centralKoszul_eq line 21
  3. theorem OAI.PD4Tensor.TruncatedForms.sigmaSelected_zero_of_not_subset line 41
  4. theorem OAI.PD4Tensor.TruncatedForms.exists_three_graph_tensor_cycle line 53
  5. def OAI.PD4Tensor.Forms.mapCoefficients line 119
  6. theorem OAI.PD4Tensor.Forms.mapCoefficients_tmul line 122
  7. theorem OAI.PD4Tensor.Forms.mapCoefficients_scalar line 125
  8. theorem OAI.PD4Tensor.Forms.mapCoefficients_oneForm line 130
  9. theorem OAI.PD4Tensor.Forms.mapCoefficients_differential line 134
  10. theorem OAI.PD4Tensor.Forms.mapCoefficients_normalCycle line 143
  11. def OAI.PD4Tensor.FiniteCoordinates.coefficientHom line 163
  12. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientHom_mk line 176
  13. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientHom_coord line 180
  14. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientHom_scalar line 185
  15. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientHom_partial line 194
  16. theorem OAI.PD4Tensor.FiniteCoordinates.specialization_eq_coefficientHom line 209
  17. def OAI.PD4Tensor.FiniteCoordinates.formsBaseChange line 236
  18. theorem OAI.PD4Tensor.FiniteCoordinates.formsBaseChange_tmul line 240
  19. theorem OAI.PD4Tensor.FiniteCoordinates.formsBaseChange_symm_tmul line 245
  20. theorem OAI.PD4Tensor.FiniteCoordinates.formsBaseChange_symm_one_tmul line 251
  21. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientMap_eq_coefficientHom line 266
  22. theorem OAI.PD4Tensor.FiniteCoordinates.partial_coefficientMap line 275
  23. theorem OAI.PD4Tensor.FiniteCoordinates.relative_differential_baseChange line 284
  24. theorem OAI.PD4Tensor.FiniteCoordinates.formsBaseChange_symm_tmul_form line 316
  25. def OAI.PD4Tensor.FiniteCoordinates.extendFormFunctional line 324
  26. theorem OAI.PD4Tensor.FiniteCoordinates.extendFormFunctional_tmul line 329
  27. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientHom_coefficientMap line 337
  28. theorem OAI.PD4Tensor.FiniteCoordinates.forms_specialization_tmul line 347
  29. theorem OAI.PD4Tensor.FiniteCoordinates.extendFormFunctional_specialization line 363