Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.ord_eq_unzero_ordHom

∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {x : ↥X} (hx : Order.coheight x = 1) {f : ↑X.functionField}
  (hf : f ≠ 0), AlgebraicGeometry.Scheme.ord f x = Multiplicative.toAdd (WithZero.unzero ⋯)

Defined in

Mathlib.AlgebraicGeometry.OrderOfVanishing

Cited by

3 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsIntegralAlgebraicGeometry.IsLocallyNoetherian