Commit 2023-08-06 20:21 dc0a7a96

View on Github →

feat: change definition of natCast in Cardinal to lift #(Fin n) (#6384) The new definition is conceptually more satisfactory. By also changing the definition of the Zero and One instances, we get ((0 : ℕ) : Cardinal) = 0 and ((1 : ℕ) : Cardinal) = 1 definitionally (which wasn't true before), which is in practice more convenient than definitional equality with PEmpty or PUnit.

Estimated changes

modified theorem Cardinal.lift_mk_fin
modified theorem Cardinal.lift_one
modified theorem Cardinal.lift_zero
modified theorem Cardinal.mk_fintype
modified theorem Cardinal.mk_option
modified theorem Cardinal.nat_succ
modified theorem Cardinal.power_one
modified theorem Ordinal.cof_zero
modified theorem Ordinal.card_one
modified theorem Ordinal.card_zero