Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-02 23:29 bb5e5986

View on Github →

feat(set_theory/cardinal_ordinal): Add simp lemmas for aleph (#13056)

Estimated changes

Modified src/set_theory/cardinal_ordinal.lean

added theorem cardinal.aleph_add_aleph

added theorem cardinal.aleph_mul_aleph

added theorem cardinal.aleph_mul_omega

added theorem cardinal.max_aleph_eq

added theorem cardinal.omega_mul_aleph