English
Let K be a field with a valuation v into NNReal, and O a ring with O-algebra structure inside K. For f and g in PreTilt(O, p), the auxiliary valuation is multiplicative: valAux(K, v, O, p; f · g) = valAux(K, v, O, p; f) · valAux(K, v, O, p; g).
Русский
Пусть K — поле с вальюацией v в NNReal, O — кольцо с алгебральной структурой над O и p натуральное, простое. Для элементов f и g из PreTilt(O, p) вспомогательная оценка удовлетворяет свойству мультипликативности: valAux(K, v, O, p; f · g) = valAux(K, v, O, p; f) · valAux(K, v, O, p; g).
LaTeX
$$$valAux(K,v,O,p)(f \cdot g) = valAux(K,v,O,p)(f) \cdot valAux(K,v,O,p)(g)$$$
Lean4
theorem valAux_mul (f g : PreTilt O p) : valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g :=
by
by_cases hf : f = 0
· rw [hf, zero_mul, valAux_zero, zero_mul]
by_cases hg : g = 0
· rw [hg, mul_zero, valAux_zero, mul_zero]
obtain ⟨m, hm⟩ : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext h
obtain ⟨n, hn⟩ : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h
replace hm := coeff_ne_zero_of_le hm (le_max_left m n)
replace hn := coeff_ne_zero_of_le hn (le_max_right m n)
have hfg : coeff _ _ (max m n + 1) (f * g) ≠ 0 :=
by
rw [RingHom.map_mul]
refine ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_
· rw [← RingHom.map_pow, coeff_pow_p f]; assumption
· rw [← RingHom.map_pow, coeff_pow_p g]; assumption
rw [valAux_eq hv (coeff_add_ne_zero hm 1), valAux_eq hv (coeff_add_ne_zero hn 1), valAux_eq hv hfg]
rw [RingHom.map_mul] at hfg ⊢; rw [ModP.preVal_mul hv hfg, mul_pow]
