mathlib

dccab1c9 - feat(algebra/ring/basic): Generalize theorems on distributivity (#14140)

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](https://leanprover-community.github.io/mathlib_docs/set_theory/ordinal/arithmetic.html#ordinal.mul_add).