Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.ord

{X : AlgebraicGeometry.Scheme} →
  [inst : AlgebraicGeometry.IsIntegral X] → [AlgebraicGeometry.IsLocallyNoetherian X] → ↑X.functionField → ↥X → ℤ

The order of vanishing of an element of the function field of a locally Noetherian integral scheme at a point. This has a junk value of 0 if f = 0 or if coheight z ≠ 1.

Defined in

Mathlib.AlgebraicGeometry.OrderOfVanishing

Cited by

12 results in Mathlib

Foundations

Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.IsIntegralAlgebraicGeometry.IsLocallyNoetherian