Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-29 21:58 2a929f24

View on Github →

feat(algebra/ne_zero): typeclass for n ≠ 0 (#11033)

Estimated changes

modified theorem nonzero_of_invertible
added theorem ne_zero.ne'
added theorem ne_zero.ne
added theorem ne_zero.of_gt
added theorem ne_zero.of_injective'
added theorem ne_zero.of_injective
added theorem ne_zero.of_map
added theorem ne_zero.of_ne_zero_coe
added theorem ne_zero.of_not_dvd
added theorem ne_zero.of_pos
added theorem ne_zero_iff
added theorem not_ne_zero