English
If b is a non-zero divisor, the order of vanishing satisfies ord(a b) = ord(a) + ord(b).
Русский
Если b не является нулевым делителем, то ord(a b) = ord(a) + ord(b).
LaTeX
$$Ring.ord R (a * b) = Ring.ord R a + Ring.ord R b$$
Lean4
/-- The order of vanishing of `a * b` is the order of vanishing of `a` plus the order
of vanishing of `b`.
-/
theorem ord_mul {a b : R} (hb : b ∈ nonZeroDivisors R) : Ring.ord R (a * b) = Ring.ord R a + Ring.ord R b :=
by
have :=
Module.length_eq_add_of_exact (Ideal.mulQuot b (Ideal.span { a })) (Ideal.quotOfMul b (Ideal.span { a }))
(Ideal.mulQuot_injective (Ideal.span { a }) hb) (Ideal.quotOfMul_surjective (Ideal.span { a }))
(Ideal.exact_mulQuot_quotOfMul (Ideal.span { a }))
simp only [Ring.ord, ← this]
have lem : (({ b } : Set R) • Ideal.span { a }) = Ideal.span {b * a} := by
simp [← Ideal.submodule_span_eq, Submodule.set_smul_span]
have : (({ b } : Set R) • Ideal.span { a }) = b • Ideal.span { a } :=
Submodule.singleton_set_smul (Ideal.span { a }) b
rw [this] at lem
rw [lem, mul_comm]
