Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-06 12:19 d490ad10

View on Github →

move(set_theory/ordinal/cantor_normal_form): move CNF to a new file (#14563) We move the API for the Cantor Normal Form to a new file, in preparation for an API expansion.

Estimated changes

deleted def ordinal.CNF
deleted theorem ordinal.CNF_foldr
deleted theorem ordinal.CNF_fst_le
deleted theorem ordinal.CNF_fst_le_log
deleted theorem ordinal.CNF_lt_snd
deleted theorem ordinal.CNF_ne_zero
deleted theorem ordinal.CNF_pairwise
deleted theorem ordinal.CNF_rec_ne_zero
deleted theorem ordinal.CNF_rec_zero
deleted theorem ordinal.CNF_snd_lt
deleted theorem ordinal.CNF_sorted
deleted theorem ordinal.CNF_zero
deleted theorem ordinal.one_CNF
deleted theorem ordinal.zero_CNF
added def ordinal.CNF
added theorem ordinal.CNF_foldr
added theorem ordinal.CNF_fst_le
added theorem ordinal.CNF_fst_le_log
added theorem ordinal.CNF_lt_snd
added theorem ordinal.CNF_ne_zero
added theorem ordinal.CNF_pairwise
added theorem ordinal.CNF_rec_zero
added theorem ordinal.CNF_snd_lt
added theorem ordinal.CNF_sorted
added theorem ordinal.CNF_zero
added theorem ordinal.one_CNF
added theorem ordinal.zero_CNF