English
For all x,y in R, the v-adic valuation satisfies v(xy) = v(x) v(y).
Русский
Для любых x,y в R адическая оценка удовлетворяет v(xy) = v(x) v(y).
LaTeX
$$$v(xy) = v(x) \cdot v(y)$$$
Lean4
/-- The `v`-adic valuation of a product equals the product of the valuations. -/
theorem map_mul' (x y : R) : v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y := by
classical
simp only [intValuationDef]
by_cases hx : x = 0
· rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
· by_cases hy : y = 0
· rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
· rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithZero.coe_mul, WithZero.coe_inj, ← ofAdd_add, ←
Ideal.span_singleton_mul_span_singleton, ← Associates.mk_mul_mk, ← neg_add,
Associates.count_mul (by apply Associates.mk_ne_zero'.mpr hx) (by apply Associates.mk_ne_zero'.mpr hy)
(by apply v.associates_irreducible)]
rfl
