Commit 2023-10-14 13:46 04245a84

View on Github →

chore: remove autoImplicit in NeZero.lean (#7673) I was unaware there was some of these still lying around - should we tidy these up?

Estimated changes

modified theorem NeZero.ne'
modified theorem NeZero.ne
modified theorem eq_zero_or_neZero
modified theorem neZero_iff
modified theorem not_neZero