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.