mathlib
444b5964 - doc(ring_theory/norm) `norm_eq_prod_embeddings` docstring (#10242)

Commit

4 years ago

doc(ring_theory/norm) `norm_eq_prod_embeddings` docstring (#10242) Co-authored-by: Chris Birkbeck <56166236+CBirkbeck@users.noreply.github.com>

Author

CBirkbeck

Parents