Commit 2025-01-08 12:28 5cd69fff

View on Github →

feat(RingTheory/PowerSeries): basic API about truncation (#20426)

Estimated changes

Modified Mathlib/RingTheory/MvPowerSeries/Trunc.lean

added theorem MvPowerSeries.trunc_C_mul

added theorem MvPowerSeries.trunc_map

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem PowerSeries.algebraMap_eq

Modified Mathlib/RingTheory/PowerSeries/Trunc.lean

added theorem PowerSeries.trunc_C_mul

added theorem PowerSeries.trunc_map

added theorem PowerSeries.trunc_mul_C

added theorem PowerSeries.trunc_one_X

added theorem PowerSeries.trunc_one_left