Commit 2022-07-08 22:50 fefd449d
View on Github →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.