Commit 2023-09-22 17:22 fc88c1f4

View on Github →

feat(RingTheory/PowerSeries): add lemmas on formal power series (#7294) Add lemmas on truncation of pormal power series

Estimated changes

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem Polynomial.eval₂_C_X_eq_coe

modified def PowerSeries.C

modified theorem PowerSeries.C_eq_algebraMap

modified def PowerSeries.X

modified theorem PowerSeries.X_dvd_iff

modified theorem PowerSeries.X_eq

modified theorem PowerSeries.X_ne_zero

modified theorem PowerSeries.X_pow_dvd_iff

modified theorem PowerSeries.X_pow_eq

modified theorem PowerSeries.X_prime

modified theorem PowerSeries.algebraMap_apply'

modified theorem PowerSeries.algebraMap_apply

modified def PowerSeries.coeff

modified theorem PowerSeries.coeff_C

modified theorem PowerSeries.coeff_C_mul

modified theorem PowerSeries.coeff_X

modified theorem PowerSeries.coeff_X_pow

modified theorem PowerSeries.coeff_X_pow_mul'

modified theorem PowerSeries.coeff_X_pow_mul

modified theorem PowerSeries.coeff_X_pow_self

added theorem PowerSeries.coeff_coe_trunc_of_lt

modified theorem PowerSeries.coeff_invOfUnit

modified theorem PowerSeries.coeff_inv_aux

modified theorem PowerSeries.coeff_map

modified theorem PowerSeries.coeff_mul

modified theorem PowerSeries.coeff_mul_C

modified theorem PowerSeries.coeff_mul_X_pow'

modified theorem PowerSeries.coeff_mul_X_pow

added theorem PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc

added theorem PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂

modified theorem PowerSeries.coeff_mul_of_lt_order

modified theorem PowerSeries.coeff_mul_one_sub_of_lt_order

modified theorem PowerSeries.coeff_one

modified theorem PowerSeries.coeff_one_X

modified theorem PowerSeries.coeff_rescale

modified theorem PowerSeries.coeff_succ_X_mul

modified theorem PowerSeries.coeff_succ_mul_X

modified theorem PowerSeries.coeff_trunc

modified theorem PowerSeries.coeff_zero_X

modified theorem PowerSeries.coeff_zero_X_mul

modified theorem PowerSeries.coeff_zero_eq_constantCoeff_apply

modified theorem PowerSeries.coeff_zero_mul_X

modified theorem PowerSeries.coeff_zero_one

modified theorem PowerSeries.commute_X

modified def PowerSeries.constantCoeff

modified theorem PowerSeries.constantCoeff_invOfUnit

added theorem PowerSeries.degree_trunc_lt

modified theorem PowerSeries.eq_X_mul_shift_add_const

modified theorem PowerSeries.eq_shift_mul_X_add_const

modified theorem PowerSeries.eq_zero_or_eq_zero_of_mul_eq_zero

modified theorem PowerSeries.evalNegHom_X

added theorem PowerSeries.eval₂_trunc_eq_sum_range

modified theorem PowerSeries.ext

modified theorem PowerSeries.ext_iff

modified def PowerSeries.invOfUnit

modified theorem PowerSeries.isUnit_constantCoeff

modified theorem PowerSeries.le_order

modified theorem PowerSeries.le_order_add

modified def PowerSeries.map

modified theorem PowerSeries.map_id

modified def PowerSeries.mk

modified def PowerSeries.monomial

modified theorem PowerSeries.mul_invOfUnit

added theorem PowerSeries.natDegree_trunc_lt

modified theorem PowerSeries.nat_le_order

modified def PowerSeries.order

modified theorem PowerSeries.order_X

modified theorem PowerSeries.order_X_pow

modified theorem PowerSeries.order_add_of_order_eq

modified theorem PowerSeries.order_eq

modified theorem PowerSeries.order_eq_multiplicity_X

modified theorem PowerSeries.order_eq_nat

modified theorem PowerSeries.order_eq_top

modified theorem PowerSeries.order_mul

modified theorem PowerSeries.order_mul_ge

modified theorem PowerSeries.order_one

modified theorem PowerSeries.order_zero

modified theorem PowerSeries.rescale_one

modified theorem PowerSeries.rescale_rescale

modified theorem PowerSeries.smul_eq_C_mul

modified theorem PowerSeries.span_X_isPrime

modified theorem PowerSeries.sub_const_eq_X_mul_shift

modified theorem PowerSeries.sub_const_eq_shift_mul_X

modified def PowerSeries.trunc

added theorem PowerSeries.trunc_X

added theorem PowerSeries.trunc_X_of

modified theorem PowerSeries.trunc_add

added theorem PowerSeries.trunc_coe_eq_self

added theorem PowerSeries.trunc_mul_trunc

modified theorem PowerSeries.trunc_one

added theorem PowerSeries.trunc_succ

added theorem PowerSeries.trunc_trunc

added theorem PowerSeries.trunc_trunc_mul

added theorem PowerSeries.trunc_trunc_mul_trunc

added theorem PowerSeries.trunc_trunc_of_le

added theorem PowerSeries.trunc_trunc_pow

added theorem PowerSeries.trunc_zero'

modified theorem PowerSeries.trunc_zero