English
The v-adic valuation of a sum is bounded above by the maximum of the valuations: v(x+y) ≤ max(v(x), v(y)).
Русский
Адическая оценка суммы не превосходит максимум из оценок: v(x+y) ≤ max(v(x), v(y)).
LaTeX
$$v(x+y) \le \max\{v(x), v(y)\}$$
Lean4
/-- The `v`-adic valuation of a sum is bounded above by the maximum of the valuations. -/
theorem map_add_le_max' (x y : R) : v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y) := by
classical
by_cases hx : x = 0
· rw [hx, zero_add]
conv_rhs => rw [intValuationDef, if_pos (Eq.refl _)]
rw [max_eq_right (WithZero.zero_le (v.intValuationDef y))]
· by_cases hy : y = 0
· rw [hy, add_zero]
conv_rhs => rw [max_comm, intValuationDef, if_pos (Eq.refl _)]
rw [max_eq_right (WithZero.zero_le (v.intValuationDef x))]
· by_cases hxy : x + y = 0
· rw [intValuationDef, if_pos hxy]; exact zero_le'
· rw [v.intValuationDef_if_neg hxy, v.intValuationDef_if_neg hx, v.intValuationDef_if_neg hy, WithZero.le_max_iff,
intValuation.le_max_iff_min_le]
set nmin :=
min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { x })).factors)
((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { y })).factors)
have h_dvd_x : x ∈ v.asIdeal ^ nmin :=
by
rw [← Associates.le_singleton_iff x nmin _, Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hx) _]
· exact min_le_left _ _
apply v.associates_irreducible
have h_dvd_y : y ∈ v.asIdeal ^ nmin :=
by
rw [← Associates.le_singleton_iff y nmin _, Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hy) _]
· exact min_le_right _ _
apply v.associates_irreducible
have h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y}) :=
by
rw [Associates.le_singleton_iff]
exact Ideal.add_mem (v.asIdeal ^ nmin) h_dvd_x h_dvd_y
rw [Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hxy) _] at h_dvd_xy
· exact h_dvd_xy
apply v.associates_irreducible
