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
