Additive valuations of finite products #
An additive valuation turns products into sums. Mathlib records this for a product of two
elements (AddValuation.map_mul) and for powers (AddValuation.map_pow); this file records the
finite-product form, which is what a valuation computation on a factorised element such as
f'(x) = ∏ (x - σ x) uses.
Main results #
AddValuation.map_prod:v (∏ i ∈ s, f i) = ∑ i ∈ s, v (f i).
@[simp]
theorem
AddValuation.map_prod
{R : Type u_1}
{Γ₀ : Type u_2}
[CommRing R]
[LinearOrderedAddCommMonoidWithTop Γ₀]
(v : AddValuation R Γ₀)
{ι : Type u_3}
(s : Finset ι)
(f : ι → R)
:
An additive valuation of a finite product is the sum of the valuations of the factors.