Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.injective.prod

Modification history

2020-07-10 04:14
src/data/prod.lean
chore(logic/embedding): reuse proofs from `data.*` (#3341) …
Deleted function.injective.prodView on Github →
2020-02-26 10:53
src/data/prod.lean
chore(data/prod): rename `injective_prod` to `injective.prod` (#2058) …
Added function.injective.prodView on Github →