Commit 2025-08-21 10:55 003d61d7

View on Github →

chore(RingTheory/(Mv)PowerSeries): use implicit parameters in monomial, coeff, map, C, and constantCoeff (#27889) Just like what we did for Polynomial, MvPolynomial, and HahnSeries.

Estimated changes

modified theorem PowerSeries.heval_C
modified theorem HahnSeries.ofPowerSeries_C
modified theorem PowerSeries.coe_C
modified theorem MvPolynomial.coe_C
modified theorem MvPolynomial.coeff_coe
modified theorem MvPowerSeries.X_def
modified theorem MvPowerSeries.X_pow_eq
modified theorem MvPowerSeries.coeff_apply
modified theorem MvPowerSeries.coeff_map
modified theorem MvPowerSeries.coeff_one
modified theorem MvPowerSeries.coeff_smul
modified theorem MvPowerSeries.coeff_zero
modified theorem MvPowerSeries.coeff_zero_C
modified theorem MvPowerSeries.coeff_zero_X
modified theorem MvPowerSeries.ext
modified theorem MvPowerSeries.map_C
modified theorem MvPowerSeries.map_X
modified theorem MvPowerSeries.map_comp
modified theorem MvPowerSeries.map_id
modified theorem MvPowerSeries.map_monomial
modified theorem MvPowerSeries.smul_eq_C_mul
modified theorem MvPowerSeries.eval₂_C
modified theorem MvPowerSeries.C_inv
modified theorem MvPowerSeries.invOfUnit_eq'
modified theorem MvPowerSeries.invOfUnit_eq
modified theorem MvPowerSeries.invOfUnit_mul
modified theorem MvPowerSeries.inv_eq_zero
modified theorem MvPowerSeries.mul_invOfUnit
modified theorem MvPowerSeries.le_order
modified theorem MvPowerSeries.nat_le_order
modified theorem MvPowerSeries.order_le
modified theorem MvPowerSeries.trunc_C
modified theorem Polynomial.coe_C
modified theorem Polynomial.coeff_coe
modified theorem PowerSeries.C_eq_algebraMap
modified theorem PowerSeries.C_injective
modified theorem PowerSeries.X_dvd_iff
modified theorem PowerSeries.X_eq
modified theorem PowerSeries.X_pow_eq
modified theorem PowerSeries.algebraMap_eq
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_def
modified theorem PowerSeries.coeff_map
modified theorem PowerSeries.coeff_mk
modified theorem PowerSeries.coeff_monomial
modified theorem PowerSeries.coeff_mul_C
modified theorem PowerSeries.coeff_ne_zero_C
modified theorem PowerSeries.coeff_one
modified theorem PowerSeries.coeff_one_X
modified theorem PowerSeries.coeff_one_mul
modified theorem PowerSeries.coeff_succ_C
modified theorem PowerSeries.coeff_zero_C
modified theorem PowerSeries.coeff_zero_X
modified theorem PowerSeries.coeff_zero_one
modified theorem PowerSeries.constantCoeff_C
modified theorem PowerSeries.constantCoeff_X
modified theorem PowerSeries.ext
modified theorem PowerSeries.map_C
modified theorem PowerSeries.monomial_eq_mk
modified theorem PowerSeries.rescale_X
modified theorem PowerSeries.rescale_zero
modified theorem PowerSeries.smul_eq_C_mul
modified theorem PowerSeries.derivativeFun_C
modified theorem PowerSeries.derivative_C
modified theorem PowerSeries.le_gaussNorm
modified theorem PowerSeries.C_inv
modified theorem PowerSeries.invOfUnit_eq'
modified theorem PowerSeries.invOfUnit_eq
modified theorem PowerSeries.invOfUnit_mul
modified theorem PowerSeries.inv_eq_inv_aux
modified theorem PowerSeries.inv_eq_zero
modified theorem PowerSeries.mul_invOfUnit
modified theorem PowerSeries.coeff_order
modified theorem PowerSeries.le_order
modified theorem PowerSeries.nat_le_order
modified theorem PowerSeries.order_le
modified theorem PowerSeries.trunc_C
modified theorem PowerSeries.trunc_C_mul
modified theorem PowerSeries.trunc_mul_C
modified theorem PowerSeries.trunc_one_left
modified theorem PowerSeries.coeff_exp