English
Under suitable hypotheses, the two definitions of vanishing order agree as elements are viewed in the fraction field.
Русский
При подходящих условиях два определения порядка исчезновения согласуются при переходе к полю дробей.
LaTeX
$$eq ordFrac ordFrac ordMonoidWithZeroHom$$
Lean4
/-- Order of vanishing function for elements of the fraction field defined as the extension of
`CommRing.ordMonoidWithZeroHom` to the field of fractions.
-/
@[stacks 02MD]
noncomputable def ordFrac : K →*₀ ℤᵐ⁰ :=
letI f := (toLocalizationMap (nonZeroDivisors R) K).lift₀ (ordMonoidWithZeroHom R)
haveI : ∀ (y : ↥(nonZeroDivisors R)), IsUnit (ordMonoidWithZeroHom R ↑y) :=
by
intro y
simp only [isUnit_iff_ne_zero, ne_eq]
simp [ordMonoidWithZeroHom, ord]
have := Module.length_ne_top_iff.mpr <| isFiniteLength_quotient_span_singleton R y.2
have : ∀ k, (WithZero.map' (AddMonoidHom.toMultiplicative (Nat.castAddMonoidHom ℤ))) k = 0 ↔ k = 0 :=
by
intro k
cases k
all_goals simp
simpa [this]
f this
