Commit 2025-12-15 11:03 c14f394d

View on Github →

feat: cardinality of Hahn series (#32640) This is a very preliminary development; most of the PR is really just lemmas about HahnSeries.support. This will be needed in the CGT repo, to define surreal Hahn series as the subfield of real, small Hahn series over their own order dual.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

modified theorem HahnSeries.support_add_subset

added theorem HahnSeries.support_neg_subset

added theorem HahnSeries.support_smul_subset

added theorem HahnSeries.support_sub_subset

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added theorem HahnSeries.support_map_subset

added theorem HahnSeries.support_mk

added theorem HahnSeries.support_truncLT

added theorem HahnSeries.support_truncLT_subset

Created Mathlib/RingTheory/HahnSeries/Cardinal.lean

added def HahnSeries.cardSupp

added theorem HahnSeries.cardSupp_add_le

added theorem HahnSeries.cardSupp_congr

added theorem HahnSeries.cardSupp_map_le

added theorem HahnSeries.cardSupp_mono

added theorem HahnSeries.cardSupp_mul_le

added theorem HahnSeries.cardSupp_neg

added theorem HahnSeries.cardSupp_neg_le

added theorem HahnSeries.cardSupp_single_le

added theorem HahnSeries.cardSupp_single_of_ne

added theorem HahnSeries.cardSupp_smul_le

added theorem HahnSeries.cardSupp_sub_le

added theorem HahnSeries.cardSupp_truncLT_le

added theorem HahnSeries.cardSupp_zero

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

added theorem HahnSeries.support_mul_subset

deleted theorem HahnSeries.support_mul_subset_add_support

Modified Mathlib/RingTheory/HahnSeries/Summable.lean