Commit 2021-04-28 01:28 d40a60c8

feat(logic/embedding): add function.embedding.coe_injective (#7383) Prior art for this lemma name: linear_map.coe_injective