mathlib3
d40a60c8 - feat(logic/embedding): add function.embedding.coe_injective (#7383)

Commit

4 years ago

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

Author

eric-wieser

Parents