Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.injective_prod

Modification history

2020-02-26 10:53

src/data/prod.lean

chore(data/prod): rename `injective_prod` to `injective.prod` (#2058) …

Deleted function.injective_prod View on Github →

2019-07-09 20:34

src/data/prod.lean

refactor(topology/*): define and use dense_inducing (#1193) …

Added function.injective_prod View on Github →