Local norms of $w$-adic integers are $v$-adic integers

Let $K/F$ be a finite extension of number fields, let $v$ be a finite place of $F$ and $w$ a finite place of $K$, with completions $F_v$ and $K_w$ and valuation rings $\mathcal O_v \subseteq F_v$, $\mathcal O_w \subseteq K_w$. Suppose $K_w$ carries an $F_v$-algebra structure which is continuous and extends $F \hookrightarrow K \hookrightarrow K_w$ (this happens exactly when $w \mid v$). Then for every $z \in \mathcal O_w$,

Consequently the local norm restricts to a continuous homomorphism $\mathcal O_w^\times \to \mathcal O_v^\times$ on unit groups, which is the building block of semilocal norm maps.

Formalization Note The $F_v$-algebra structure on $K_w$ is a hypothesis (Algebra, ContinuousSMul, IsScalarTower F F_v K_w), as in Mathlib's NumberField/Completion/FinitePlace.lean; it is unique when it exists.