doc(ring_theory/norm) norm_eq_prod_embeddings docstring (#10242)

Co-authored-by: Chris Birkbeck <56166236+CBirkbeck@users.noreply.github.com>

src/ring_theory/norm.lean

@@ -225,6 +225,9 @@ end
 
 variable (K)
 
+/-- For `L/K` a finite separable extension of fields and `E` an algebraically closed extension
+of `K`, the norm (down to `K`) of an element `x` of `L` is equal to the product of the images
+of `x` over all the `K`-embeddings `σ`  of `L` into `E`. -/
 lemma norm_eq_prod_embeddings [finite_dimensional K L] [is_separable K L] [is_alg_closed E]
   {x : L} : algebra_map K E (norm K x) = ∏ σ : L →ₐ[K] E, σ x :=
 begin