Local–global norm formula $N_{K/F}(x)=\prod_{w\mid v}N_{K_w/F_v}(x)$

Let $K/F$ be a finite extension of number fields, let $v$ be a finite place of $F$, i.e. a nonzero prime ideal of $\mathcal O_F$, and let $F_v$ be the $v$-adic completion of $F$. For each prime $w$ of $\mathcal O_K$ lying over $v$ (written $w \mid v$), let $K_w$ be the $w$-adic completion of $K$, regarded as an $F_v$-algebra via the continuous extension of $F \hookrightarrow K \hookrightarrow K_w$. Then for every $x \in K$, the image of the global norm in $F_v$ is the product of the local norms:

This identity connects global norms with local norms at a finite place; it is used for instance to show that the semilocal norm map on local units sends diagonally embedded global units to diagonally embedded global norms, and in the local–global analysis of norm groups.

Formalization Note Mathlib at this revision provides no canonical algebra structure $F_v \to K_w$. As in Mathlib's own NumberField.HeightOneSpectrum API (the instance Module.Finite Kv Lw in NumberField/Completion/FinitePlace.lean), the statement takes, for each $w$, an arbitrary $F_v$-algebra structure on $K_w$ that is continuous (ContinuousSMul) and compatible with $F \to K$ (IsScalarTower F F_v K_w). Since $F$ is dense in $F_v$, such a structure is unique, and it exists (the continuous extension of $F \hookrightarrow K \hookrightarrow K_w$) exactly when $w \mid v$; so the hypotheses just name the canonical embedding. Primes $w \mid v$ are the height-one primes $w$ of $\mathcal O_K$ with w.asIdeal.LiesOver v.asIdeal; there are finitely many, and the finite sum/product is written with finsum/finprod so that no finiteness hypothesis is needed.