Commit 2024-02-15 23:16 6af8f3b3

View on Github →

refactor(Cardinal): redefine toNat and toPartENat (#10472) Redefine these operations in terms of toENat.

Estimated changes

deleted theorem Cardinal.toNat_toENat
deleted theorem Cardinal.toPartENat_cast
modified theorem Cardinal.one_toNat
added theorem Cardinal.toNat_add
deleted theorem Cardinal.toNat_cast
modified theorem Cardinal.toNat_eq_iff
modified theorem Cardinal.toNat_eq_ofNat
modified theorem Cardinal.toNat_eq_one
added theorem Cardinal.toNat_injOn
modified theorem Cardinal.toNat_mul
added theorem Cardinal.toNat_natCast
added theorem Cardinal.toNat_ofENat
added theorem Cardinal.toNat_toENat
modified theorem Cardinal.zero_toNat