Herbrand quotient one for U over a cohomologically trivial V

Let $G$ be a finite cyclic group acting on an abelian group $M$ (written multiplicatively) by a multiplicative distributive action, so that each $g \in G$ acts as a group automorphism of $M$. Let $U$ and $V$ be subgroups of $M$ with $V \le U$, both stable under the action elementwise ($g \cdot x \in U$ for all $g \in G$, $x \in U$, and likewise for $V$), and assume that $V$, viewed inside $U$, has finite index. Assume further that $V$ is cohomologically trivial in degrees $1$ and $2$ in the following explicit form: every $f : G \to M$ with all values in $V$ satisfying the multiplicative $1$-cocycle condition IsMulCocycle₁ is of the form $f(g) = (g \cdot x)/x$ for some $x \in V$; and every $f : G \times G \to M$ with all values in $V$ satisfying the multiplicative $2$-cocycle condition IsMulCocycle₂ satisfies $f(g,h) = (g \cdot x(h)) \, x(g) / x(gh)$ for some $x : G \to M$ with all values in $V$. Finally, let a multiplicative distributive action of $G$ on the subgroup $U$ be given which is compatible with the action on $M$, i.e. $(g \cdot u : M) = g \cdot (u : M)$ for all $g \in G$, $u \in U$. Then, for the $\mathbb{Z}[G]$-representation Rep.ofMulDistribMulAction G U attached to this action, $H^1$ and $H^2$ are both finite and $\#H^1(G,U) = \#H^2(G,U)$.

This is the statement that the Herbrand quotient $h(U) = \#H^1/\#H^2$ of a cyclic group acting on $U$ equals $1$ whenever $U$ contains a $G$-stable subgroup of finite index with vanishing $H^1$ and $H^2$; it is obtained from the short exact sequence $1 \to V \to U \to U/V \to 1$ together with groupCohomology.natCard_H1_eq_natCard_H2_of_shortExact_of_subsingleton_of_finite. It serves the computation of norm groups of unit groups in unramified layers, and is used in the proof of the existence of elements of prescribed norm in fields obtained by adjoining roots of unity to a $p$-adic field.