mathlib3

5cf7a1c5 - feat (algebra/group/prod): Showing that embed_product is injective (#14247)

feat (algebra/group/prod): Showing that embed_product is injective (#14247) Proves that `embed_product` is injective. Co-authored-by: laughinggas <58670661+laughinggas@users.noreply.github.com>