Commit 2022-03-15 11:51 7a02c9e6

View on Github →

fix(set_theory/ordinal_arithmetic): remove redundant hypothesis from CNF_rec (#12680) The hypothesis in question was a theorem that could be deduced.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

deleted theorem ordinal.CNF_aux

modified theorem ordinal.CNF_fst_le_log

modified theorem ordinal.CNF_pairwise

modified theorem ordinal.CNF_snd_lt

modified theorem ordinal.CNF_sorted

added theorem ordinal.mod_opow_log_lt_self

modified theorem ordinal.one_CNF