Norm expansion N(1+γ)=1+Tr γ+Nγ+Tr δ in prime degree

Let $B$ be a commutative ring and $G$ a finite group acting on $B$ by ring automorphisms (a MulSemiringAction), and suppose that the cardinality $\mathrm{Nat.card}\,G$ of $G$ is prime. Then for every $\gamma \in B$ there exists an element $\delta$ lying in the ideal of $B$ generated by the set of all products $(\sigma_1 \bullet \gamma)(\sigma_2 \bullet \gamma)$ with $\sigma_1, \sigma_2 \in G$ distinct, such that the identity

holds in $B$, the products and sums being the finprod and finsum of the indicated families over all of $G$ (which reduce to ordinary finite products and sums since $G$ is finite). Thus the product of $1 + \sigma \bullet \gamma$ over $G$ equals $1$, plus the trace of $\gamma$, plus the norm of $\gamma$, plus the trace of an element of the ideal generated by the products of two distinct conjugates of $\gamma$. No invertibility or division is assumed, so the statement covers both the tame and the wild case.

This is the standard expansion of the norm $N(1+\gamma) = 1 + \mathrm{Tr}(\gamma) + N(\gamma) + \mathrm{Tr}(\delta)$ in a cyclic layer of prime degree, with the error term $\delta$ controlled by products of two distinct conjugates of $\gamma$; the primality of $|G|$ enters because translation permutes freely the subsets of $G$ of intermediate size, so that their contributions assemble into a trace. It is used in the ramification-theoretic estimates for discrete valuation rings with a prime-order group action, namely IsDiscreteValuationRing.exists_finset_card_le_forall_exists_sub_mul_finprod_smul_mem_pow_of_prime_card, IsDiscreteValuationRing.exists_sub_one_mem_and_finprod_smul_sub_mem_of_jump_lt_of_prime_card and IsDiscreteValuationRing.finprod_smul_sub_one_mem_maximalIdeal_pow_of_sub_one_mem_pow_herbrand_of_prime_card.