Commit 2020-07-06 14:12 33b6cba0

refactor(*): replace nonzero with nontrivial (#3296) Introduce a typeclass nontrivial saying that a type has at least two distinct elements, and use it instead of the predicate nonzero requiring that 0 is different from 1. These two predicates are equivalent in monoids with zero, which cover essentially all relevant ring-like situations, but nontrivial applies also to say that a vector space is nontrivial, for instance. Along the way, fix some quirks in the alebraic hierarchy (replacing fields zero_ne_one in many structures with extending nontrivial, for instance). Also, quadratic_reciprocity was timing out. I guess it was just below the threshold before the refactoring, and some of the changes related to typeclass inference made it just above after the change. So, I squeeze_simped it, going from 47s to 1.7s on my computer. Zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/nonsingleton/near/202865366