Commit 2025-05-12 12:04 86d0bf37

View on Github →

feat(RingTheory/PowerSeries/*): various small results (#24678)

Mathlib/RingTheory/PowerSeries/CoeffMulMem.lean: some results on the coefficients of multiplication of two power series
Mathlib/RingTheory/PowerSeries/Trunc.lean: add two results eq_shift_mul_X_pow_add_trunc and eq_X_pow_mul_shift_add_trunc generalizing eq_shift_mul_X_add_const and eq_X_mul_shift_add_const
Mathlib/Data/ENat/Basic.lean: add ENat.lift_eq_toNat which seems convenient (?)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.lift_eq_toNat_of_lt_top

Created Mathlib/RingTheory/PowerSeries/CoeffMulMem.lean

added theorem PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'

added theorem PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal

added theorem PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal'

added theorem PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal

added theorem PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal'

added theorem PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal

Modified Mathlib/RingTheory/PowerSeries/Trunc.lean

added theorem PowerSeries.eq_X_pow_mul_shift_add_trunc

added theorem PowerSeries.eq_shift_mul_X_pow_add_trunc