Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-23 10:20 275dd0f3

View on Github →

feat(algebra/ne_zero): add helper methods (#14286) Also golfs the inspiration for one of these, and cleans up some code around the area.

Estimated changes

added theorem eq_zero_or_ne_zero
modified theorem ne_zero.of_injective
added theorem ne_zero.pos
modified theorem ne_zero.trans