OAI/Algebra/FrobeniusObstruction/LinearChange.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.Frobenius.augmentation line 14
  2. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.augmentation_coordinate line 18
  3. def OAI.BoundaryOnly.FormalObstruction.Frobenius.maximalIdeal line 23
  4. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.maximalIdeal_nilpotent line 26
  5. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.augmentation_comp line 40
  6. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.endomorphism_difference_mem line 49
  7. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.bijective_of_tangent_identity line 57
  8. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.monomial_mem_coordinate_pow line 66
  9. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.maximalIdeal_eq_span line 83
  10. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.bijective_of_coordinate_first_jet line 110
  11. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.endomorphism_pow_mem line 123
  12. def OAI.BoundaryOnly.FormalObstruction.Frobenius.linearCoordinates line 137
  13. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.augmentation_linearCoordinates line 141
  14. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.linearCoordinates_pow line 149
  15. def OAI.BoundaryOnly.FormalObstruction.Frobenius.linearSubst line 155
  16. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.linearSubst_coordinate line 158
  17. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.linearSubst_comp line 162
  18. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.linearSubst_one line 171
  19. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.linearSubst_injective line 177
  20. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.bijective_of_invertible_first_jet line 189
  21. def OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentCoeff line 226
  22. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentCoeff_mk line 233
  23. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentCoeff_coordinate line 237
  24. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.tangentCoeff_one line 241
  25. def OAI.BoundaryOnly.FormalObstruction.Frobenius.firstJetError line 247
  26. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.firstJetError_apply line 251
  27. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.firstJetError_one line 256
  28. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.firstJetError_coordinate line 259
  29. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.firstJetError_mem_square line 265
  30. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.bijective_of_tangent_matrix line 304
  31. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.derivation_chain_rule line 322
  32. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.partial_chain_rule line 358