mathlib

fefd449d - feat(set_theory/ordinal/arithmetic): tweak `type_add` and `type_mul` (#15193)

feat(set_theory/ordinal/arithmetic): tweak `type_add` and `type_mul` (#15193) This renames `type_mul` to the more accurate `type_prod_lex`, and renames `type_add` to `type_sum_lex` and reverses the order of the equality so that the two lemmas match.