OAI/AlgebraicGeometry/NumericalDimension/BoundaryDiscrepancies.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Boundary Discrepancies.

  1. lemma OAI.NumericalDimensionOne.quotient_ringSmooth_of_affine_subscheme line 20
  2. theorem OAI.NumericalDimensionOne.formallySmooth_quotient_localization line 44
  3. theorem OAI.NumericalDimensionOne.affine_hypersurface_stalk_formallySmooth line 75
  4. lemma OAI.NumericalDimensionOne.open_top_germ line 128
  5. theorem OAI.NumericalDimensionOne.affineOpen_hypersurface_stalk_formallySmooth line 137
  6. lemma OAI.NumericalDimensionOne.alternating_update_basis line 183
  7. theorem OAI.NumericalDimensionOne.topDifferentialMap_divisible_of_primitive line 196
  8. theorem OAI.NumericalDimensionOne.smooth_hypersurface_differential_primitive line 257
  9. def OAI.NumericalDimensionOne.IsSmoothEffectiveCartierDivisor line 331
  10. lemma OAI.NumericalDimensionOne.formallySmooth_smooth_stalk line 340
  11. lemma OAI.NumericalDimensionOne.order_stalk_irreducible line 360
  12. lemma OAI.NumericalDimensionOne.order_stalk_unit_mul_pow line 369
  13. lemma OAI.NumericalDimensionOne.order_stalk_divisible_pow_lower_bound line 380
  14. theorem OAI.NumericalDimensionOne.smooth_boundary_discrepancy_bound line 400