Commit 2026-10-01 14:50 c7eec140
View on Github →feat(SetTheory/Ordinal): definition of addition and multiplication (#43588)
We prove theorems Ordinal.type_lt_sum_lex and Ordinal.type_lt_prod_lex, which characterize addition and multiplication on ordinals.