Commit 2024-01-18 13:29 05dc8889

View on Github →

feat(Cardinal): define conversion to/from ENat (#9792)

Estimated changes

added theorem Cardinal.enat_gc
added theorem Cardinal.lift_ofENat
added theorem Cardinal.nat_eq_ofENat
added theorem Cardinal.nat_le_ofENat
added theorem Cardinal.nat_lt_ofENat
added def Cardinal.ofENat
added theorem Cardinal.ofENat_add
added theorem Cardinal.ofENat_eq_nat
added theorem Cardinal.ofENat_eq_one
added theorem Cardinal.ofENat_inj
added theorem Cardinal.ofENat_le_nat
added theorem Cardinal.ofENat_le_one
added theorem Cardinal.ofENat_lt_nat
added theorem Cardinal.ofENat_mono
added theorem Cardinal.ofENat_mul
added theorem Cardinal.ofENat_nat
added theorem Cardinal.ofENat_ofNat
added theorem Cardinal.ofENat_one
added theorem Cardinal.ofENat_pos
added theorem Cardinal.ofENat_top
added theorem Cardinal.ofENat_zero
added theorem Cardinal.one_eq_ofENat
added theorem Cardinal.one_le_ofENat
added theorem Cardinal.one_lt_ofENat
added theorem Cardinal.range_ofENat
added theorem Cardinal.toENatAux_gc
added theorem Cardinal.toENatAux_nat
added theorem Cardinal.toENat_eq_nat
added theorem Cardinal.toENat_eq_one
added theorem Cardinal.toENat_eq_top
added theorem Cardinal.toENat_injOn
added theorem Cardinal.toENat_nat
added theorem Cardinal.toENat_ofENat
added theorem Cardinal.toNat_toENat