Finite-field sum decompositions

Elementary identities relating sums over the units of a finite field to sums over the whole field. This module is deliberately below the character-sum and MCM layers so that both can use the same finite-field infrastructure.

theorem KasamiCyclicAdditive.sum_units_eq_sum {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {M : Type u_2} [AddCommMonoid M] (f : K → M) (hf : f 0 = 0) : ∑ b : Kˣ, f ↑b = ∑ a : K, f a

A sum over the unit group equals the sum over the whole field, for a function vanishing at 0.

theorem KasamiCyclicAdditive.sum_units_add {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {M : Type u_2} [AddCommMonoid M] (f : K → M) : f 0 + ∑ b : Kˣ, f ↑b = ∑ a : K, f a

Splitting off the value at 0 from a sum over the whole field.