Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ne_zero.nat_of_injective

Modification history

2022-11-04 20:50

src/algebra/ne_zero.lean

chore(algebra/ne_zero): move the dependencies out (#17177) …

Modified ne_zero.nat_of_injective View on Github →

2022-01-10 16:17

src/algebra/ne_zero.lean

feat(data/nat/cast): generalize to `fun_like` (#11128)

Added ne_zero.nat_of_injective View on Github →