OAI/Algebra/MarkedTensor/Holonomy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cubic nilpotence for reference holonomies and quotient ideals.

  1. def OAI.BoundaryOnly.Holonomy.referenceOver line 18
  2. theorem OAI.BoundaryOnly.Holonomy.cubic_nilpotence_reference line 24
  3. lemma OAI.BoundaryOnly.Holonomy.cube_sum_pullback line 40
  4. lemma OAI.BoundaryOnly.Holonomy.slope_deviation_mem line 56
  5. lemma OAI.BoundaryOnly.Holonomy.map_deviation_entry line 74
  6. theorem OAI.BoundaryOnly.Holonomy.cubic_nilpotence_mod_ideal line 84