Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pnat.coe_injective

Modification history

2022-11-06 23:41
src/data/pnat/basic.lean
refactor(*): supremum of several recent refactoring PRs (#17381) …
Modified pnat.coe_injectiveView on Github →
2021-04-12 23:25
src/data/pnat/basic.lean
refactor(algebra/group/defs): remove left-right_cancel_comm_monoids (#7134) …
Added pnat.coe_injectiveView on Github →