Commit 2023-05-22 16:35 3d924717

View on Github →

feat: port RingTheory.PowerSeries.Basic (#4167)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/PowerSeries/Basic.lean

added def MvPolynomial.coeToMvPowerSeries.algHom

added theorem MvPolynomial.coeToMvPowerSeries.algHom_apply

added def MvPolynomial.coeToMvPowerSeries.ringHom

added theorem MvPolynomial.coeToMvPowerSeries.ringHom_apply

added theorem MvPolynomial.coe_C

added theorem MvPolynomial.coe_X

added theorem MvPolynomial.coe_add

added theorem MvPolynomial.coe_bit0

added theorem MvPolynomial.coe_bit1

added theorem MvPolynomial.coe_def

added theorem MvPolynomial.coe_eq_one_iff

added theorem MvPolynomial.coe_eq_zero_iff

added theorem MvPolynomial.coe_inj

added theorem MvPolynomial.coe_injective

added theorem MvPolynomial.coe_monomial

added theorem MvPolynomial.coe_mul

added theorem MvPolynomial.coe_one

added theorem MvPolynomial.coe_pow

added theorem MvPolynomial.coe_zero

added theorem MvPolynomial.coeff_coe

added def MvPolynomial.toMvPowerSeries

added def MvPowerSeries.C

added theorem MvPowerSeries.C_inv

added def MvPowerSeries.X

added theorem MvPowerSeries.X_def

added theorem MvPowerSeries.X_dvd_iff

added theorem MvPowerSeries.X_inj

added theorem MvPowerSeries.X_inv

added theorem MvPowerSeries.X_pow_dvd_iff

added theorem MvPowerSeries.X_pow_eq

added theorem MvPowerSeries.algebraMap_apply''

added theorem MvPowerSeries.algebraMap_apply'

added theorem MvPowerSeries.algebraMap_apply

added theorem MvPowerSeries.c_eq_algebraMap

added def MvPowerSeries.coeff

added theorem MvPowerSeries.coeff_C

added theorem MvPowerSeries.coeff_C_mul

added theorem MvPowerSeries.coeff_X

added theorem MvPowerSeries.coeff_X_pow

added theorem MvPowerSeries.coeff_add_monomial_mul

added theorem MvPowerSeries.coeff_add_mul_monomial

added theorem MvPowerSeries.coeff_comp_monomial

added theorem MvPowerSeries.coeff_index_single_X

added theorem MvPowerSeries.coeff_index_single_self_X

added theorem MvPowerSeries.coeff_inv

added theorem MvPowerSeries.coeff_invOfUnit

added theorem MvPowerSeries.coeff_inv_aux

added theorem MvPowerSeries.coeff_map

added theorem MvPowerSeries.coeff_monomial

added theorem MvPowerSeries.coeff_monomial_mul

added theorem MvPowerSeries.coeff_monomial_ne

added theorem MvPowerSeries.coeff_monomial_same

added theorem MvPowerSeries.coeff_mul

added theorem MvPowerSeries.coeff_mul_C

added theorem MvPowerSeries.coeff_mul_monomial

added theorem MvPowerSeries.coeff_one

added theorem MvPowerSeries.coeff_smul

added theorem MvPowerSeries.coeff_trunc

added theorem MvPowerSeries.coeff_truncFun

added theorem MvPowerSeries.coeff_zero

added theorem MvPowerSeries.coeff_zero_C

added theorem MvPowerSeries.coeff_zero_X

added theorem MvPowerSeries.coeff_zero_X_mul

added theorem MvPowerSeries.coeff_zero_eq_constantCoeff

added theorem MvPowerSeries.coeff_zero_eq_constantCoeff_apply

added theorem MvPowerSeries.coeff_zero_mul_X

added theorem MvPowerSeries.coeff_zero_one

added theorem MvPowerSeries.commute_X

added theorem MvPowerSeries.commute_monomial

added def MvPowerSeries.constantCoeff

added theorem MvPowerSeries.constantCoeff_C

added theorem MvPowerSeries.constantCoeff_X

added theorem MvPowerSeries.constantCoeff_comp_C

added theorem MvPowerSeries.constantCoeff_inv

added theorem MvPowerSeries.constantCoeff_invOfUnit

added theorem MvPowerSeries.constantCoeff_map

added theorem MvPowerSeries.constantCoeff_one

added theorem MvPowerSeries.constantCoeff_zero

added theorem MvPowerSeries.eq_of_coeff_monomial_ne_zero

added theorem MvPowerSeries.ext

added theorem MvPowerSeries.ext_iff

added def MvPowerSeries.invOfUnit

added theorem MvPowerSeries.invOfUnit_eq'

added theorem MvPowerSeries.invOfUnit_eq

added theorem MvPowerSeries.inv_eq_zero

added theorem MvPowerSeries.isUnit_constantCoeff

added def MvPowerSeries.map

added theorem MvPowerSeries.map_C

added theorem MvPowerSeries.map_X

added theorem MvPowerSeries.map_comp

added theorem MvPowerSeries.map_id

added theorem MvPowerSeries.map_monomial

added def MvPowerSeries.monomial

added theorem MvPowerSeries.monomial_def

added theorem MvPowerSeries.monomial_mul_monomial

added theorem MvPowerSeries.monomial_zero_eq_C

added theorem MvPowerSeries.monomial_zero_eq_C_apply

added theorem MvPowerSeries.monomial_zero_one

added theorem MvPowerSeries.mul_invOfUnit

added theorem MvPowerSeries.smul_eq_C_mul

added theorem MvPowerSeries.smul_inv

added def MvPowerSeries.trunc

added def MvPowerSeries.truncFun

added theorem MvPowerSeries.trunc_c

added theorem MvPowerSeries.trunc_one

added theorem MvPowerSeries.zero_inv

added def MvPowerSeries

added def Polynomial.ToPowerSeries

added def Polynomial.coeToPowerSeries.algHom

added theorem Polynomial.coeToPowerSeries.algHom_apply

added def Polynomial.coeToPowerSeries.ringHom

added theorem Polynomial.coeToPowerSeries.ringHom_apply

added theorem Polynomial.coe_C

added theorem Polynomial.coe_X

added theorem Polynomial.coe_add

added theorem Polynomial.coe_bit0

added theorem Polynomial.coe_bit1

added theorem Polynomial.coe_def

added theorem Polynomial.coe_eq_one_iff

added theorem Polynomial.coe_eq_zero_iff

added theorem Polynomial.coe_inj

added theorem Polynomial.coe_injective

added theorem Polynomial.coe_monomial

added theorem Polynomial.coe_mul

added theorem Polynomial.coe_one

added theorem Polynomial.coe_pow

added theorem Polynomial.coe_zero

added theorem Polynomial.coeff_coe

added theorem Polynomial.constantCoeff_coe

added def PowerSeries.C

added theorem PowerSeries.C_eq_algebraMap

added theorem PowerSeries.C_inv

added def PowerSeries.X

added theorem PowerSeries.X_dvd_iff

added theorem PowerSeries.X_eq

added theorem PowerSeries.X_inv

added theorem PowerSeries.X_ne_zero

added theorem PowerSeries.X_pow_dvd_iff

added theorem PowerSeries.X_pow_eq

added theorem PowerSeries.X_pow_order_dvd

added theorem PowerSeries.X_prime

added theorem PowerSeries.algebraMap_apply''

added theorem PowerSeries.algebraMap_apply'

added theorem PowerSeries.algebraMap_apply

added def PowerSeries.coeff

added theorem PowerSeries.coeff_C

added theorem PowerSeries.coeff_C_mul

added theorem PowerSeries.coeff_C_mul_X_pow

added theorem PowerSeries.coeff_X

added theorem PowerSeries.coeff_X_pow

added theorem PowerSeries.coeff_X_pow_mul'

added theorem PowerSeries.coeff_X_pow_mul

added theorem PowerSeries.coeff_X_pow_self

added theorem PowerSeries.coeff_comp_monomial

added theorem PowerSeries.coeff_def

added theorem PowerSeries.coeff_inv

added theorem PowerSeries.coeff_invOfUnit

added theorem PowerSeries.coeff_inv_aux

added theorem PowerSeries.coeff_map

added theorem PowerSeries.coeff_mk

added theorem PowerSeries.coeff_monomial

added theorem PowerSeries.coeff_monomial_same

added theorem PowerSeries.coeff_mul

added theorem PowerSeries.coeff_mul_C

added theorem PowerSeries.coeff_mul_X_pow'

added theorem PowerSeries.coeff_mul_X_pow

added theorem PowerSeries.coeff_mul_of_lt_order

added theorem PowerSeries.coeff_mul_one_sub_of_lt_order

added theorem PowerSeries.coeff_mul_prod_one_sub_of_lt_order

added theorem PowerSeries.coeff_of_lt_order

added theorem PowerSeries.coeff_one

added theorem PowerSeries.coeff_one_X

added theorem PowerSeries.coeff_order

added theorem PowerSeries.coeff_rescale

added theorem PowerSeries.coeff_smul

added theorem PowerSeries.coeff_succ_X_mul

added theorem PowerSeries.coeff_succ_mul_X

added theorem PowerSeries.coeff_trunc

added theorem PowerSeries.coeff_zero_C

added theorem PowerSeries.coeff_zero_X

added theorem PowerSeries.coeff_zero_X_mul

added theorem PowerSeries.coeff_zero_eq_constantCoeff

added theorem PowerSeries.coeff_zero_eq_constantCoeff_apply

added theorem PowerSeries.coeff_zero_mul_X

added theorem PowerSeries.coeff_zero_one

added theorem PowerSeries.commute_X

added def PowerSeries.constantCoeff

added theorem PowerSeries.constantCoeff_C

added theorem PowerSeries.constantCoeff_X

added theorem PowerSeries.constantCoeff_comp_C

added theorem PowerSeries.constantCoeff_inv

added theorem PowerSeries.constantCoeff_invOfUnit

added theorem PowerSeries.constantCoeff_one

added theorem PowerSeries.constantCoeff_zero

added theorem PowerSeries.eq_X_mul_shift_add_const

added theorem PowerSeries.eq_inv_iff_mul_eq_one

added theorem PowerSeries.eq_mul_inv_iff_mul_eq

added theorem PowerSeries.eq_shift_mul_X_add_const

added theorem PowerSeries.eq_zero_or_eq_zero_of_mul_eq_zero

added theorem PowerSeries.evalNegHom_X

added theorem PowerSeries.exists_coeff_ne_zero_iff_ne_zero

added theorem PowerSeries.ext

added theorem PowerSeries.ext_iff

added def PowerSeries.invOfUnit

added theorem PowerSeries.invOfUnit_eq'

added theorem PowerSeries.invOfUnit_eq

added theorem PowerSeries.inv_eq_iff_mul_eq_one

added theorem PowerSeries.inv_eq_inv_aux

added theorem PowerSeries.inv_eq_zero

added theorem PowerSeries.isUnit_constantCoeff

added theorem PowerSeries.le_order

added theorem PowerSeries.le_order_add

added def PowerSeries.map

added theorem PowerSeries.map_C

added theorem PowerSeries.map_X

added theorem PowerSeries.map_comp

added theorem PowerSeries.map_id

added def PowerSeries.mk

added def PowerSeries.monomial

added theorem PowerSeries.monomial_eq_mk

added theorem PowerSeries.monomial_zero_eq_C

added theorem PowerSeries.monomial_zero_eq_C_apply

added theorem PowerSeries.mul_invOfUnit

added theorem PowerSeries.nat_le_order

added def PowerSeries.order

added theorem PowerSeries.order_X

added theorem PowerSeries.order_X_pow

added theorem PowerSeries.order_add_of_order_eq

added theorem PowerSeries.order_eq

added theorem PowerSeries.order_eq_multiplicity_X

added theorem PowerSeries.order_eq_nat

added theorem PowerSeries.order_eq_top

added theorem PowerSeries.order_finite_iff_ne_zero

added theorem PowerSeries.order_le

added theorem PowerSeries.order_monomial

added theorem PowerSeries.order_monomial_of_ne_zero

added theorem PowerSeries.order_mul

added theorem PowerSeries.order_mul_ge

added theorem PowerSeries.order_one

added theorem PowerSeries.order_zero

added theorem PowerSeries.rescale_X

added theorem PowerSeries.rescale_injective

added theorem PowerSeries.rescale_mk

added theorem PowerSeries.rescale_mul

added theorem PowerSeries.rescale_neg_one_X

added theorem PowerSeries.rescale_one

added theorem PowerSeries.rescale_rescale

added theorem PowerSeries.rescale_zero

added theorem PowerSeries.rescale_zero_apply

added theorem PowerSeries.smul_eq_C_mul

added theorem PowerSeries.smul_inv

added theorem PowerSeries.span_X_isPrime

added theorem PowerSeries.sub_const_eq_X_mul_shift

added theorem PowerSeries.sub_const_eq_shift_mul_X

added def PowerSeries.trunc

added theorem PowerSeries.trunc_C

added theorem PowerSeries.trunc_add

added theorem PowerSeries.trunc_one

added theorem PowerSeries.trunc_zero

added theorem PowerSeries.zero_inv

added def PowerSeries