Commit 2022-07-20 16:22 6102220d

View on Github →

style(set_theory/ordinal/cantor_normal_form): rename hypotheses (#15229) We rename hypotheses with names like o0, b0, and b1 to more standard ho and hb.

Estimated changes

Modified src/set_theory/ordinal/cantor_normal_form.lean

modified theorem ordinal.CNF_foldr

modified theorem ordinal.CNF_lt_snd

modified theorem ordinal.CNF_ne_zero

modified theorem ordinal.CNF_rec_ne_zero

modified theorem ordinal.CNF_rec_zero

modified theorem ordinal.CNF_snd_lt

modified theorem ordinal.one_CNF