OAI/AlgebraicGeometry/NumericalDimension/NormalCrossings.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Normal Crossings.

  1. lemma OAI.NumericalDimensionOne.topDifferentialMap_coefficient_pullback line 31
  2. lemma OAI.NumericalDimensionOne.canonical_germ_generator line 50
  3. lemma OAI.NumericalDimensionOne.canonical_ramification_coefficient line 94
  4. theorem OAI.NumericalDimensionOne.independent_boundary_discrepancy_bound_scheme line 177
  5. theorem OAI.NumericalDimensionOne.independent_boundary_discrepancy_bound line 249
  6. def OAI.NumericalDimensionOne.IsSimpleNormalCrossingsDivisorFamily line 277
  7. theorem OAI.NumericalDimensionOne.snc_boundary_discrepancy_bound line 289
  8. lemma OAI.NumericalDimensionOne.IsQCartierPullback.sum line 321
  9. theorem OAI.NumericalDimensionOne.snc_boundary_isKlt line 336
  10. def OAI.NumericalDimensionOne.IsSimpleNormalCrossingsDivisorFamilyOver line 415
  11. theorem OAI.NumericalDimensionOne.snc_boundary_discrepancy_bound_scheme line 428
  12. lemma OAI.NumericalDimensionOne.snc_fractional_discrepancy_bound_scheme line 462