Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-19 08:21 0bb665cc

View on Github →

chore(ring_theory/power_series): review, golf (#5431)

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.prod_ite_index

added theorem finset.prod_sigma'

Modified src/analysis/analytic/composition.lean

Modified src/data/complex/exponential.lean

Modified src/data/nat/enat.lean

modified theorem enat.coe_lt_top

Modified src/number_theory/arithmetic_function.lean

Modified src/ring_theory/power_series.lean

modified def mv_power_series.coeff

added theorem mv_power_series.coeff_add_monomial_mul

added theorem mv_power_series.coeff_add_mul_monomial

deleted theorem mv_power_series.coeff_monomial'

added theorem mv_power_series.coeff_monomial_mul

added theorem mv_power_series.coeff_monomial_ne

added theorem mv_power_series.coeff_monomial_same

added theorem mv_power_series.coeff_mul_monomial

added theorem mv_power_series.eq_of_coeff_monomial_ne_zero

added theorem mv_power_series.map_C

added theorem mv_power_series.map_X

added theorem mv_power_series.map_monomial

modified def mv_power_series.monomial

modified theorem mv_power_series.monomial_zero_eq_C

added theorem mv_power_series.monomial_zero_one

modified def power_series.coeff

deleted theorem power_series.coeff_monomial'

added theorem power_series.coeff_monomial_same

modified def power_series.monomial

modified theorem power_series.monomial_zero_eq_C

modified theorem power_series.order_eq_top