Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-30 05:20 af53c9d7

View on Github →

chore(algebra/ring): move some classes to group_with_zero (#3232) Move nonzero, mul_zero_class and no_zero_divisors to group_with_zero: these classes don't need (+).

Estimated changes

added theorem commute.zero_left
added theorem commute.zero_right
added theorem mul_eq_zero
added theorem mul_eq_zero_comm
added theorem mul_ne_zero
added theorem mul_ne_zero_comm
added theorem mul_ne_zero_iff
added theorem mul_self_eq_zero
added theorem mul_zero
added theorem one_ne_zero
added theorem semiconj_by.zero_left
added theorem semiconj_by.zero_right
added theorem zero_eq_mul
added theorem zero_eq_mul_self
added theorem zero_mul
added theorem zero_ne_one
deleted theorem commute.zero_left
deleted theorem commute.zero_right
modified theorem left_distrib
deleted theorem mul_eq_zero
deleted theorem mul_eq_zero_comm
deleted theorem mul_ne_zero
deleted theorem mul_ne_zero_comm
deleted theorem mul_ne_zero_iff
deleted theorem mul_self_eq_zero
deleted theorem mul_zero
deleted theorem one_ne_zero
modified theorem right_distrib
deleted theorem semiconj_by.zero_left
deleted theorem semiconj_by.zero_right
deleted theorem zero_eq_mul
deleted theorem zero_eq_mul_self
deleted theorem zero_mul
deleted theorem zero_ne_one