Commit 2024-02-29 12:38 73d45f44

View on Github →

split power series in several files (#10866) This PR split the files devoted to power series (especially RingTheory/PowerSeries/Basic) into several ones:

  • RingTheory/MvPowerSeries/Basic - initial definitions (multivariate)
  • RingTheory/MvPowerSeries/Trunc - truncation
  • RingTheory/MvPowerSeries/Inverse - stuff pertaining to inverses
  • RingTheory/PowerSeries/Basic - initial definitions (univariate)
  • RingTheory/PowerSeries/Trunc - truncation
  • RingTheory/PowerSeries/Inverse - stuff pertaining to inverses
  • RingTheory/PowerSeries/Order - stuff pertaining to order it remains to adjust the other files (PowerSeries/Derivative and PowerSeries/WellKnown)

Estimated changes

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_inj
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 MvPowerSeries.C
added def MvPowerSeries.X
added theorem MvPowerSeries.X_def
added theorem MvPowerSeries.X_inj
added theorem MvPowerSeries.X_pow_eq
added theorem MvPowerSeries.coeff_C
added theorem MvPowerSeries.coeff_X
added theorem MvPowerSeries.ext
added theorem MvPowerSeries.ext_iff
added theorem MvPowerSeries.map_C
added theorem MvPowerSeries.map_X
added theorem MvPowerSeries.map_comp
added theorem MvPowerSeries.map_id
added def MvPowerSeries
added theorem MvPowerSeries.C_inv
added theorem MvPowerSeries.X_inv
added theorem MvPowerSeries.smul_inv
added theorem MvPowerSeries.zero_inv
added theorem MvPowerSeries.trunc_c
deleted theorem MvPolynomial.coe_C
deleted theorem MvPolynomial.coe_X
deleted theorem MvPolynomial.coe_add
deleted theorem MvPolynomial.coe_bit0
deleted theorem MvPolynomial.coe_bit1
deleted theorem MvPolynomial.coe_def
deleted theorem MvPolynomial.coe_inj
deleted theorem MvPolynomial.coe_monomial
deleted theorem MvPolynomial.coe_mul
deleted theorem MvPolynomial.coe_one
deleted theorem MvPolynomial.coe_pow
deleted theorem MvPolynomial.coe_zero
deleted theorem MvPolynomial.coeff_coe
deleted def MvPowerSeries.C
deleted theorem MvPowerSeries.C_inv
deleted def MvPowerSeries.X
deleted theorem MvPowerSeries.X_def
deleted theorem MvPowerSeries.X_dvd_iff
deleted theorem MvPowerSeries.X_inj
deleted theorem MvPowerSeries.X_inv
deleted theorem MvPowerSeries.X_pow_eq
deleted def MvPowerSeries.coeff
deleted theorem MvPowerSeries.coeff_C
deleted theorem MvPowerSeries.coeff_C_mul
deleted theorem MvPowerSeries.coeff_X
deleted theorem MvPowerSeries.coeff_X_pow
deleted theorem MvPowerSeries.coeff_inv
deleted theorem MvPowerSeries.coeff_map
deleted theorem MvPowerSeries.coeff_mul
deleted theorem MvPowerSeries.coeff_mul_C
deleted theorem MvPowerSeries.coeff_one
deleted theorem MvPowerSeries.coeff_prod
deleted theorem MvPowerSeries.coeff_smul
deleted theorem MvPowerSeries.coeff_trunc
deleted theorem MvPowerSeries.coeff_zero
deleted theorem MvPowerSeries.commute_X
deleted theorem MvPowerSeries.ext
deleted theorem MvPowerSeries.ext_iff
deleted theorem MvPowerSeries.inv_eq_zero
deleted def MvPowerSeries.map
deleted theorem MvPowerSeries.map_C
deleted theorem MvPowerSeries.map_X
deleted theorem MvPowerSeries.map_comp
deleted theorem MvPowerSeries.map_id
deleted theorem MvPowerSeries.smul_inv
deleted def MvPowerSeries.trunc
deleted theorem MvPowerSeries.trunc_c
deleted theorem MvPowerSeries.trunc_one
deleted theorem MvPowerSeries.zero_inv
deleted def MvPowerSeries
deleted theorem PowerSeries.C_inv
deleted theorem PowerSeries.X_inv
deleted theorem PowerSeries.coeff_inv
deleted theorem PowerSeries.coeff_inv_aux
deleted theorem PowerSeries.coeff_order
deleted theorem PowerSeries.coeff_trunc
deleted theorem PowerSeries.invOfUnit_eq'
deleted theorem PowerSeries.invOfUnit_eq
deleted theorem PowerSeries.inv_eq_zero
deleted theorem PowerSeries.le_order
deleted theorem PowerSeries.le_order_add
deleted theorem PowerSeries.mul_invOfUnit
deleted theorem PowerSeries.nat_le_order
deleted def PowerSeries.order
deleted theorem PowerSeries.order_X
deleted theorem PowerSeries.order_X_pow
deleted theorem PowerSeries.order_eq
deleted theorem PowerSeries.order_eq_nat
deleted theorem PowerSeries.order_eq_top
deleted theorem PowerSeries.order_le
deleted theorem PowerSeries.order_mul
deleted theorem PowerSeries.order_mul_ge
deleted theorem PowerSeries.order_one
deleted theorem PowerSeries.order_zero
deleted theorem PowerSeries.smul_inv
deleted def PowerSeries.trunc
deleted theorem PowerSeries.trunc_C
deleted theorem PowerSeries.trunc_X
deleted theorem PowerSeries.trunc_X_of
deleted theorem PowerSeries.trunc_add
deleted theorem PowerSeries.trunc_one
deleted theorem PowerSeries.trunc_succ
deleted theorem PowerSeries.trunc_trunc
deleted theorem PowerSeries.trunc_zero'
deleted theorem PowerSeries.trunc_zero
deleted theorem PowerSeries.zero_inv
added theorem PowerSeries.C_inv
added theorem PowerSeries.X_inv
added theorem PowerSeries.coeff_inv
added theorem PowerSeries.smul_inv
added theorem PowerSeries.zero_inv
added theorem PowerSeries.le_order
added theorem PowerSeries.order_X
added theorem PowerSeries.order_eq
added theorem PowerSeries.order_le
added theorem PowerSeries.order_mul
added theorem PowerSeries.order_one
added theorem PowerSeries.order_zero
added theorem PowerSeries.trunc_C
added theorem PowerSeries.trunc_X
added theorem PowerSeries.trunc_X_of
added theorem PowerSeries.trunc_add
added theorem PowerSeries.trunc_one
added theorem PowerSeries.trunc_succ
added theorem PowerSeries.trunc_zero