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 <42eef2908a3747a81ba273aacddc7d78480b2c1f@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib