OAI/AlgebraicGeometry/NumericalDimension/FactorialDivisors.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Factorial Divisors.

  1. lemma OAI.NumericalDimensionOne.affine_equation_of_generization_orders line 18
  2. theorem OAI.NumericalDimensionOne.isCartierDivisor_of_factorial_stalks line 46
  3. lemma OAI.NumericalDimensionOne.exists_local_order_bound line 100
  4. def OAI.NumericalDimensionOne.localVanishingOrder line 113
  5. lemma OAI.NumericalDimensionOne.localVanishingOrder_not_mem line 118
  6. lemma OAI.NumericalDimensionOne.localVanishingOrder_mem_iff line 123
  7. lemma OAI.NumericalDimensionOne.localVanishingOrder_unit_mul line 140
  8. theorem OAI.NumericalDimensionOne.PrincipalLocal.isDomain_of_principal_maximal line 167
  9. theorem OAI.NumericalDimensionOne.TwoParameters.quotient_principal_domain line 212
  10. theorem OAI.NumericalDimensionOne.PrincipalQuotientLift.principal_of_quotient line 270
  11. theorem OAI.NumericalDimensionOne.SurfaceFactorial.factorial_of_dimension_two line 317
  12. theorem OAI.NumericalDimensionOne.SurfaceFactorial.factorial_of_dimension_le_two line 370
  13. theorem OAI.NumericalDimensionOne.factorial_stalk_of_smooth_surface line 404
  14. theorem OAI.NumericalDimensionOne.isCartierDivisor_smooth_surface line 423
  15. theorem OAI.NumericalDimensionOne.pointClosure_affineIdeal line 440
  16. theorem OAI.NumericalDimensionOne.closedImmersion_stalk_ker line 474
  17. def OAI.NumericalDimensionOne.closedImmersion_stalkQuotient line 505
  18. lemma OAI.NumericalDimensionOne.pointClosure_specializes line 523
  19. theorem OAI.NumericalDimensionOne.pointClosure_stalk_ker line 529
  20. def OAI.NumericalDimensionOne.pointClosure_stalkEquiv line 547