OAI/Algebra/MarkedTensor/TripleProducts.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Triple coordinate products and cubic nilpotence of local holonomy ideals.

  1. def OAI.BoundaryOnly.Holonomy.tripleEvaluation line 17
  2. def OAI.BoundaryOnly.Holonomy.entriesSubmodule line 64
  3. lemma OAI.BoundaryOnly.Holonomy.span_map_mem line 73
  4. lemma OAI.BoundaryOnly.Holonomy.span_three_mem line 80
  5. def OAI.BoundaryOnly.Holonomy.rankMap line 90
  6. lemma OAI.BoundaryOnly.Holonomy.coordinate_product_mem line 97
  7. def OAI.BoundaryOnly.Holonomy.deviationIdeal line 131
  8. def OAI.BoundaryOnly.Holonomy.coordinateIdeal line 133
  9. lemma OAI.BoundaryOnly.Holonomy.deviation_mem line 137
  10. lemma OAI.BoundaryOnly.Holonomy.coordinates_mem line 141
  11. lemma OAI.BoundaryOnly.Holonomy.coordinateIdeal_le line 148
  12. lemma OAI.BoundaryOnly.Holonomy.trace_deviation_mem line 155
  13. lemma OAI.BoundaryOnly.Holonomy.scalar_mem line 171
  14. lemma OAI.BoundaryOnly.Holonomy.traceless_mem line 180
  15. lemma OAI.BoundaryOnly.Holonomy.deviation_le_coordinates line 189
  16. lemma OAI.BoundaryOnly.Holonomy.deviationIdeal_eq_coordinates line 209
  17. lemma OAI.BoundaryOnly.Holonomy.coordinate_cube_le line 223
  18. theorem OAI.BoundaryOnly.Holonomy.cubic_nilpotence_local line 242