Top exterior power of multiplication by x is N_{B/A}(x)

Let $A$ and $B$ be commutative rings and let $B$ be an $A$-algebra. Let $\iota$ be a finite index type and let $b$ be a basis of $B$ as an $A$-module indexed by $\iota$, so that $B$ is free of finite rank over $A$; let $n$ be a natural number with $\operatorname{card}\iota = n$. Then for every $x \in B$ and every element $w$ of the $n$-th exterior power $\bigwedge^n_A B$, the $A$-linear endomorphism of $\bigwedge^n_A B$ obtained by applying the $n$-th exterior power functor exteriorPower.map to the $A$-linear map $b \mapsto x b$ of left multiplication by $x$ on $B$ sends $w$ to $N_{B/A}(x) \cdot w$, where $N_{B/A}(x)$ is Algebra.norm A x. Equivalently, on the top exterior power of $B$ this endomorphism is the scalar $N_{B/A}(x)$; the conclusion is stated pointwise in $w$ rather than as an equality of linear maps. The basis $b$ and the cardinality hypothesis enter only as the witness that $B$ is free of rank $n$ over $A$.

This is the determinantal description of the algebra norm read on the top exterior power: on $\bigwedge^n_A B$, multiplication by $x$ acts through $N_{B/A}(x)$. It is used in the project in the computation of the ideal generated by an algebra norm under a discrete valuation ring hypothesis, Ideal.span_algebraNorm_eq_of_ker_eq_span_of_isDiscreteValuationRing.