Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-29 22:20 f95e8090

View on Github →

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)

Estimated changes

modified theorem not_is_unit_zero
modified theorem char_p.ring_char_ne_one
modified theorem eq_zero_of_mul_self_eq_zero
added theorem nonzero.of_ne
modified theorem one_ne_zero
modified theorem pred_ne_self
modified theorem succ_ne_self
modified theorem units.coe_ne_zero
deleted theorem units.ne_zero
modified theorem zero_ne_one
modified theorem pequiv.to_matrix_injective
modified theorem polynomial.monic.ne_zero
modified theorem card_units_lt
modified theorem ring_hom.not_one_mem_ker