mathlib

5f3f01f9 - feat(set_theory/ordinal_arithmetic): Proved `add_log_le_log_mul` (#11228)

feat(set_theory/ordinal_arithmetic): Proved `add_log_le_log_mul` (#11228) That is, `log b u + log b v ≤ log b (u * v)`. The other direction holds only when `b ≠ 2` and `b` is principal multiplicative, and will be added at a much later PR.