Orthogonality for the additive valuation of a discrete valuation ring #
A finite sum of elements with pairwise distinct finite additive valuations has valuation equal to
the least valuation of its terms. Zero terms cause no exception: their additive valuation is
⊤, so the same formula also covers the identically zero family.
This is the elementary nonarchimedean orthogonality principle used for power bases whose terms have valuations in distinct congruence classes.
theorem
IsDiscreteValuationRing.addVal_sum_eq_iInf_of_ne
{R : Type u_1}
[CommRing R]
[IsDomain R]
[IsDiscreteValuationRing R]
{ι : Type u_2}
[Fintype ι]
(a : ι → R)
(h : ∀ (i j : ι), i ≠ j → a i ≠ 0 → a j ≠ 0 → (addVal R) (a i) ≠ (addVal R) (a j))
:
The additive valuation of a sum of terms with pairwise distinct finite valuations is the infimum of their valuations.