Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-23 03:11 23d61413

View on Github →

chore(algebra/ring,char_zero): generalize some lemmas (#3141) mul_eq_zero etc only need [mul_zero_class] and [no_zero_divisors]. In particular, they don't need has_neg. Also deduplicate with group_with_zero.*.

Estimated changes

deleted theorem division_ring.mul_ne_zero
modified theorem mul_inv'
deleted theorem mul_ne_zero_comm
modified theorem div_eq_zero_iff
modified theorem div_ne_zero_iff
deleted theorem mul_eq_zero'
deleted theorem mul_eq_zero_iff'
deleted theorem mul_ne_zero''
deleted theorem mul_ne_zero_comm''
deleted theorem mul_ne_zero_iff
added theorem mul_eq_zero_comm
deleted theorem mul_ne_zero'
modified theorem mul_ne_zero
deleted theorem mul_ne_zero_comm'
added theorem mul_ne_zero_comm
added theorem mul_ne_zero_iff
modified theorem mul_self_eq_zero
modified theorem zero_eq_mul_self
deleted theorem function.support_mul'
modified theorem function.support_mul