OAI/Algebra/FiniteTensor/CoordinateEquivalences.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Coordinate equivalences induced by invertible tangent matrices.

  1. theorem OAI.PD4Tensor.coordinate_error_raises line 17
  2. theorem OAI.PD4Tensor.coordinate_error_on_span line 43
  3. theorem OAI.PD4Tensor.bijective_of_identity_tangent line 68
  4. def OAI.PD4Tensor.coordinatesEquiv line 93
  5. def OAI.PD4Tensor.FiniteCoordinates.ideal line 106
  6. abbrev OAI.PD4Tensor.FiniteCoordinates.Ring line 108
  7. def OAI.PD4Tensor.FiniteCoordinates.coord line 110
  8. theorem OAI.PD4Tensor.FiniteCoordinates.coord_pow line 114
  9. def OAI.PD4Tensor.FiniteCoordinates.evaluate line 119
  10. theorem OAI.PD4Tensor.FiniteCoordinates.evaluate_coord line 128
  11. theorem OAI.PD4Tensor.FiniteCoordinates.hom_ext line 134
  12. def OAI.PD4Tensor.FiniteCoordinates.augmentationIdeal line 142
  13. theorem OAI.PD4Tensor.FiniteCoordinates.augmentation_nilpotent line 146
  14. theorem OAI.PD4Tensor.FiniteCoordinates.error_mem line 157
  15. theorem OAI.PD4Tensor.FiniteCoordinates.bijective_of_tangent_identity line 179
  16. theorem OAI.PD4Tensor.FrobeniusTruncation.linearSubst_one line 197
  17. def OAI.PD4Tensor.FrobeniusTruncation.linearEquiv line 205
  18. def OAI.PD4Tensor.FrobeniusTruncation.polynomialSubst line 219
  19. theorem OAI.PD4Tensor.FrobeniusTruncation.polynomialSubst_coord line 227
  20. theorem OAI.PD4Tensor.FrobeniusTruncation.map_idealOfVars line 236
  21. theorem OAI.PD4Tensor.FrobeniusTruncation.polynomialSubst_bijective line 245