Commit 2025-08-13 21:02 f127f08c

View on Github →

feat(RingTheory): add HahnSeries.truncLT (#27055)

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

added theorem HahnSeries.coe_truncLTLinearMap

added def HahnSeries.truncLTLinearMap

added theorem HahnSeries.truncLT_add

added theorem HahnSeries.truncLT_smul

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added theorem HahnSeries.coeff_truncLT_of_le

added theorem HahnSeries.coeff_truncLT_of_lt

added def HahnSeries.truncLT