English
valAux at 1 equals 1 by construction.
Русский
valAux(1) равно 1 по определению.
LaTeX
$$valAux(1) = 1$$
Lean4
theorem valAux_eq {f : PreTilt O p} {n : ℕ} (hfn : coeff _ _ n f ≠ 0) :
valAux K v O p f = ModP.preVal K v O p (coeff _ _ n f) ^ p ^ n :=
by
have h : ∃ n, coeff _ _ n f ≠ 0 := ⟨n, hfn⟩
rw [valAux, dif_pos h]
classical
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.find_min' h hfn)
induction k with
| zero => rfl
| succ k ih => ?_
obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (coeff (ModP O p) p (Nat.find h + k + 1) f)
have h1 : (Ideal.Quotient.mk _ x : ModP O p) ≠ 0 := hx.symm ▸ hfn
have h2 : (Ideal.Quotient.mk _ (x ^ p) : ModP O p) ≠ 0 :=
by
erw [RingHom.map_pow, hx, ← RingHom.map_pow, coeff_pow_p]
exact coeff_nat_find_add_ne_zero k
erw [ih (coeff_nat_find_add_ne_zero k), ← hx, ← coeff_pow_p, RingHom.map_pow, ← hx, ← RingHom.map_pow,
ModP.preVal_mk hv h1, ModP.preVal_mk hv h2, RingHom.map_pow, v.map_pow, ← pow_mul, pow_succ']
rfl
