Commit 2024-09-02 16:21 3631f173

View on Github →

feat(SetTheory/Cardinal/Continuum): x ^ ℵ₀ = 𝔠 for 2 ≤ x ≤ 𝔠 (#16342) We also make sure ℵ₀ and 𝔠 notation is used throughout the file.

Estimated changes

modified theorem Cardinal.nat_power_aleph0