English
The order of vanishing extends to the fraction field, giving ordFrac as a monoid with zero homomorphism to the zero-extended integers.
Русский
Порядок исчезновения можно продолжить до поля дробей, образуя ordFrac — гомоморф к нулевой дополненной целочисленной шкале.
LaTeX
$$ordFrac R$$
Lean4
/-- Zero-preserving monoid homomorphism from a nontrivial commutative ring `R` to `ℕᵐ⁰`.
Note that we cannot just use `fun x ↦ ord R x` without further assumptions on `R`.
This is because if R is finite length, then ord R 0 will be some non-top value,
meaning in this case `0` will not be mapped to `⊤`.
-/
@[stacks 02MD]
noncomputable def ordMonoidWithZeroHom [Nontrivial R] : R →*₀ ℤᵐ⁰
where
toFun x := if x ∈ nonZeroDivisors R then WithZero.map' (Nat.castAddMonoidHom ℤ).toMultiplicative (Ring.ord R x) else 0
map_zero' := by simp [nonZeroDivisors, exists_ne]
map_one' := by
simp [nonZeroDivisors, Ring.ord_one]
rfl
map_mul' := by
intro x y
split_ifs with _ _ b
· rw [← MonoidWithZeroHom.map_mul]
congr
exact ord_mul R b
all_goals simp_all [mul_mem_nonZeroDivisors]
