Commit 2022-01-04 16:45 5f3f01f9

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.