Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-28 05:34 dccab1c9

View on Github →

feat(algebra/ring/basic): Generalize theorems on distributivity (#14140) Many theorems assuming full distributivity only need left or right distributivity. We remedy this by making new left_distrib_class and right_distrib_class classes. The main motivation here is to generalize various theorems on ordinals, like ordinal.mul_add.

Estimated changes

modified theorem add_one_mul
modified theorem bit0_eq_two_mul
modified theorem distrib_three_right
modified theorem dvd_add
modified theorem left_distrib
modified theorem mul_add_one
modified theorem mul_one_add
modified theorem mul_two
modified theorem one_add_mul
modified theorem one_add_one_eq_two
modified theorem right_distrib
modified theorem two_mul