Commit 2024-02-13 12:46 c2320208

View on Github →

chore(Cardinal/Basic): split (#10466) Move toNat and toPartENat to new files. No changes in the code moved to the new files. One lemma remains in Basic but used toNat in the proof, so I changed the proof. I'm going to redefine them in terms of toENat, so I need to move them out of Basic first.

Estimated changes

deleted theorem Cardinal.aleph0_toNat
deleted theorem Cardinal.mk_toNat_eq_card
deleted theorem Cardinal.one_toNat
deleted def Cardinal.toNat
deleted def Cardinal.toNatHom
deleted theorem Cardinal.toNat_cast
deleted theorem Cardinal.toNat_congr
deleted theorem Cardinal.toNat_eq_iff
deleted theorem Cardinal.toNat_eq_ofNat
deleted theorem Cardinal.toNat_eq_one
deleted theorem Cardinal.toNat_eq_zero
deleted theorem Cardinal.toNat_lift
deleted theorem Cardinal.toNat_mul
deleted theorem Cardinal.toNat_ne_zero
deleted theorem Cardinal.toNat_ofNat
deleted theorem Cardinal.toNat_pos
deleted theorem Cardinal.toNat_surjective
deleted def Cardinal.toPartENat
deleted theorem Cardinal.toPartENat_cast
deleted theorem Cardinal.toPartENat_congr
deleted theorem Cardinal.toPartENat_lift
deleted theorem Cardinal.toPartENat_mono
deleted theorem Cardinal.zero_toNat
added theorem Cardinal.aleph0_toNat
added theorem Cardinal.one_toNat
added theorem Cardinal.toNat_cast
added theorem Cardinal.toNat_congr
added theorem Cardinal.toNat_eq_iff
added theorem Cardinal.toNat_eq_one
added theorem Cardinal.toNat_eq_zero
added theorem Cardinal.toNat_lift
added theorem Cardinal.toNat_mul
added theorem Cardinal.toNat_ne_zero
added theorem Cardinal.toNat_ofNat
added theorem Cardinal.toNat_pos
added theorem Cardinal.zero_toNat