OAI/Algebra/FiniteTensor/MovingCoordinates.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Frobenius specialization, moving substitutions and split coordinate restrictions.

  1. theorem OAI.PD4Tensor.nilEval_coefficients line 20
  2. theorem OAI.PD4Tensor.nilEval_frobenius line 68
  3. def OAI.PD4Tensor.FiniteCoordinates.constantMap line 102
  4. theorem OAI.PD4Tensor.FiniteCoordinates.constantMap_coord line 106
  5. theorem OAI.PD4Tensor.FiniteCoordinates.constantMap_mk line 110
  6. theorem OAI.PD4Tensor.FiniteCoordinates.constantMap_surjective line 116
  7. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientSpecialization_scalar line 124
  8. theorem OAI.PD4Tensor.FiniteCoordinates.pow_eq_constantMap line 149
  9. theorem OAI.PD4Tensor.FiniteCoordinates.parameter_charP line 176
  10. def OAI.PD4Tensor.FiniteCoordinates.movingSubst line 184
  11. theorem OAI.PD4Tensor.FiniteCoordinates.movingSubst_coord line 197
  12. theorem OAI.PD4Tensor.FiniteCoordinates.movingSubst_central line 207
  13. theorem OAI.PD4Tensor.FiniteCoordinates.movingSubst_bijective line 225
  14. abbrev OAI.PD4Tensor.FrobeniusTruncation.constant line 255
  15. theorem OAI.PD4Tensor.FrobeniusTruncation.constant_coord line 259
  16. theorem OAI.PD4Tensor.FrobeniusTruncation.constant_mk line 263
  17. theorem OAI.PD4Tensor.FrobeniusTruncation.constant_hom line 270
  18. def OAI.PD4Tensor.FrobeniusTruncation.tangentCoeff line 281
  19. theorem OAI.PD4Tensor.FrobeniusTruncation.tangentCoeff_mk line 285
  20. theorem OAI.PD4Tensor.FrobeniusTruncation.tangentCoeff_coord line 293
  21. theorem OAI.PD4Tensor.FrobeniusTruncation.tangentCoeff_scalar line 301
  22. theorem OAI.PD4Tensor.FrobeniusTruncation.tangentCoeff_mul line 308
  23. theorem OAI.PD4Tensor.FrobeniusTruncation.tangentCoeff_hom line 317
  24. def OAI.PD4Tensor.FrobeniusTruncation.tangentHom line 335
  25. theorem OAI.PD4Tensor.FrobeniusTruncation.tangentHom_id line 339
  26. theorem OAI.PD4Tensor.FrobeniusTruncation.tangentHom_comp line 343
  27. theorem OAI.PD4Tensor.FrobeniusTruncation.tangentHom_det_ne_zero line 350
  28. theorem OAI.PD4Tensor.FrobeniusTruncation.inverse_representatives line 364
  29. def OAI.PD4Tensor.FiniteCoordinates.renameHom line 389
  30. theorem OAI.PD4Tensor.FiniteCoordinates.renameHom_coord line 393
  31. def OAI.PD4Tensor.FiniteCoordinates.reindexEquiv line 397
  32. theorem OAI.PD4Tensor.FiniteCoordinates.reindexEquiv_coord line 405
  33. theorem OAI.PD4Tensor.FiniteCoordinates.reindexEquiv_symm_coord line 410
  34. def OAI.PD4Tensor.FiniteCoordinates.uniformLeft line 414
  35. def OAI.PD4Tensor.FiniteCoordinates.uniformInclude line 421
  36. theorem OAI.PD4Tensor.FiniteCoordinates.uniformLeft_coord line 425
  37. theorem OAI.PD4Tensor.FiniteCoordinates.uniformLeft_include line 430
  38. theorem OAI.PD4Tensor.FiniteCoordinates.uniformLeft_surjective line 440
  39. theorem OAI.PD4Tensor.FiniteCoordinates.uniformLeft_ker line 444
  40. def OAI.PD4Tensor.FiniteCoordinates.splitRestriction line 467
  41. theorem OAI.PD4Tensor.FiniteCoordinates.splitRestriction_surjective line 475
  42. theorem OAI.PD4Tensor.FiniteCoordinates.splitRestriction_ker line 484