feast(ring_theory/norm): add norm_eq_prod_embeddings (#10226)
We prove that the norm equals the product of the embeddings in an algebraically closed field.
Note that we follow a slightly different path than for the trace, since transitivity of the norm is more delicate, and we avoid it.
From flt-regular.
