Commit 2021-11-09 10:46 00d9b9f5

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.