Commit 2023-02-24 07:53 cdd500c7

View on Github →

feat: port Data.W.Cardinal (#2465)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/W/Cardinal.lean

added theorem WType.cardinal_mk_eq_sum

added theorem WType.cardinal_mk_le_max_aleph0_of_finite

added theorem WType.cardinal_mk_le_of_le