mathlib3
f95e8090 - chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop (#2847)

Commit
5 years ago
chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop (#2847) - `[nonzero_semiring α]` becomes `[semiring α] [nonzero α]` - `[nonzero_comm_semiring α]` becomes `[comm_semiring α] [nonzero α]` - `[nonzero_comm_ring α]` becomes `[comm_ring α] [nonzero α]` - `no_zero_divisors` is now a `Prop` - `units.ne_zero` (originally for `domain`) merges into `units.coe_ne_zero` (originally for `nonzero_comm_semiring`)
Author
Parents
Loading