Commit 2023-10-15 18:32 a577026a

View on Github →

feat: some simp lemmas to compute more cardinals (#7660)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.aleph0_add_ofNat

added theorem Cardinal.aleph0_mul_ofNat

added theorem Cardinal.ofNat_add_aleph0

added theorem Cardinal.ofNat_mul_aleph0

Modified Mathlib/SetTheory/Cardinal/Continuum.lean

added theorem Cardinal.continuum_add_ofNat

added theorem Cardinal.continuum_mul_ofNat

added theorem Cardinal.ofNat_add_continuum

added theorem Cardinal.ofNat_mul_continuum

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

added theorem Cardinal.nat_add_eq