OAI/Analysis/JiangSu/DimensionDrop/PresentationCertificate.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OriginalJiangSu.Multiplicities.zero_division line 14
  2. lemma OAI.OriginalJiangSu.Multiplicities.one_division line 20
  3. lemma OAI.OriginalJiangSu.Multiplicities.r_eq_mod line 26
  4. lemma OAI.OriginalJiangSu.Multiplicities.s_eq_mod line 30
  5. lemma OAI.OriginalJiangSu.Multiplicities.delta_eq_div line 34
  6. lemma OAI.OriginalJiangSu.Multiplicities.gamma_eq_div line 39
  7. lemma OAI.OriginalJiangSu.initial_dimensions line 44
  8. lemma OAI.OriginalJiangSu.successor_dimensions line 45
  9. theorem OAI.OriginalJiangSu.original_block_counts line 49
  10. theorem OAI.OriginalJiangSu.original_eigenvalues line 68
  11. theorem OAI.OriginalJiangSu.original_endpoint_fibres line 77