Finite valuation arithmetic shared by the local Wronskian estimates

theorem BGS.CorvajaZannier.FiniteValuationSums.laurent_product_valuation {K : Type u_1} [Field K] {ι : Type u_2} (s : Finset ι) (g : ι → LaurentSeries K) : (HahnSeries.addVal ℤ K) (∏ i ∈ s, g i) = ∑ i ∈ s, (HahnSeries.addVal ℤ K) (g i)

The additive Laurent valuation sends a finite product to the sum of its valuations.

theorem BGS.CorvajaZannier.FiniteValuationSums.integer_sum_coercion {ι : Type u_2} (s : Finset ι) (g : ι → ℤ) : ↑(∑ i ∈ s, g i) = ∑ i ∈ s, ↑(g i)

Coercion from integers to WithTop preserves a sum over a finset.

theorem BGS.CorvajaZannier.FiniteValuationSums.integer_sum_coercion_univ {ι : Type u_2} [Fintype ι] (g : ι → ℤ) : ↑(∑ i : ι, g i) = ∑ i : ι, ↑(g i)

Coercion from integers to WithTop preserves a sum over a finite type.