Commit 2023-12-27 08:00 2e77db72

View on Github →

feat: cardinality of Subfield.closure (#8942) Also generalize results about the cardinality of WType to be universe polymorphic. Zulip discussion about the approach

depends on: #8941

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/W/Cardinal.lean

added theorem WType.cardinal_mk_eq_sum'

modified theorem WType.cardinal_mk_eq_sum

added theorem WType.cardinal_mk_le_max_aleph0_of_finite'

added theorem WType.cardinal_mk_le_of_le'

Created Mathlib/SetTheory/Cardinal/Subfield.lean

added theorem Subfield.cardinal_mk_closure

added theorem Subfield.cardinal_mk_closure_le_max