Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-02 07:19 1f91d93b

View on Github →

chore(ring_theory/power_series): rename variables (#4361) Use R, S, T for (semi)rings and k for a field.

Estimated changes

Modified src/ring_theory/power_series.lean

modified theorem mv_polynomial.coe_C

modified theorem mv_polynomial.coe_add

modified theorem mv_polynomial.coe_monomial

modified theorem mv_polynomial.coe_mul

modified theorem mv_polynomial.coe_one

modified def mv_polynomial.coe_to_mv_power_series.ring_hom

modified theorem mv_polynomial.coe_zero

modified theorem mv_polynomial.coeff_coe

modified def mv_power_series.C

modified def mv_power_series.X

modified theorem mv_power_series.X_def

modified theorem mv_power_series.X_dvd_iff

modified theorem mv_power_series.X_inj

modified theorem mv_power_series.X_pow_dvd_iff

modified def mv_power_series.coeff

modified theorem mv_power_series.coeff_C

modified theorem mv_power_series.coeff_C_mul

modified theorem mv_power_series.coeff_inv

modified theorem mv_power_series.coeff_inv_aux

modified theorem mv_power_series.coeff_inv_of_unit

modified theorem mv_power_series.coeff_map

modified theorem mv_power_series.coeff_monomial'

modified theorem mv_power_series.coeff_monomial

modified theorem mv_power_series.coeff_mul

modified theorem mv_power_series.coeff_mul_C

modified theorem mv_power_series.coeff_smul

modified theorem mv_power_series.coeff_trunc

modified theorem mv_power_series.coeff_zero

modified theorem mv_power_series.coeff_zero_C

modified theorem mv_power_series.coeff_zero_X

modified theorem mv_power_series.coeff_zero_eq_constant_coeff_apply

modified theorem mv_power_series.coeff_zero_mul_X

modified theorem mv_power_series.coeff_zero_one

modified def mv_power_series.constant_coeff

modified theorem mv_power_series.constant_coeff_C

modified theorem mv_power_series.constant_coeff_X

modified theorem mv_power_series.constant_coeff_inv

modified theorem mv_power_series.constant_coeff_inv_of_unit

modified theorem mv_power_series.constant_coeff_map

modified theorem mv_power_series.constant_coeff_one

modified theorem mv_power_series.constant_coeff_zero

modified theorem mv_power_series.ext

modified theorem mv_power_series.ext_iff

modified theorem mv_power_series.inv_eq_zero

modified def mv_power_series.inv_of_unit

modified theorem mv_power_series.inv_of_unit_eq'

modified theorem mv_power_series.inv_of_unit_eq

modified theorem mv_power_series.is_unit_constant_coeff

modified def mv_power_series.map

modified theorem mv_power_series.map_id

modified def mv_power_series.monomial

modified theorem mv_power_series.monomial_mul_monomial

modified theorem mv_power_series.monomial_zero_eq_C

modified theorem mv_power_series.monomial_zero_eq_C_apply

modified theorem mv_power_series.mul_inv_of_unit

modified def mv_power_series.trunc

modified theorem mv_power_series.trunc_C

modified def mv_power_series.trunc_fun

modified theorem mv_power_series.trunc_one

modified def mv_power_series

modified theorem polynomial.coe_C

modified theorem polynomial.coe_add

modified theorem polynomial.coe_monomial

modified theorem polynomial.coe_mul

modified theorem polynomial.coe_one

modified def polynomial.coe_to_power_series.ring_hom

modified theorem polynomial.coe_zero

modified theorem polynomial.coeff_coe

modified def power_series.C

modified def power_series.X

modified theorem power_series.X_dvd_iff

modified theorem power_series.X_eq

modified theorem power_series.X_pow_dvd_iff

modified theorem power_series.X_pow_eq

modified theorem power_series.X_prime

modified def power_series.coeff

modified theorem power_series.coeff_C

modified theorem power_series.coeff_C_mul

modified theorem power_series.coeff_inv

modified theorem power_series.coeff_inv_aux

modified theorem power_series.coeff_inv_of_unit

modified theorem power_series.coeff_map

modified theorem power_series.coeff_mk

modified theorem power_series.coeff_monomial'

modified theorem power_series.coeff_monomial

modified theorem power_series.coeff_mul

modified theorem power_series.coeff_mul_C

modified theorem power_series.coeff_of_lt_order

modified theorem power_series.coeff_one_X

modified theorem power_series.coeff_order

modified theorem power_series.coeff_smul

modified theorem power_series.coeff_succ_mul_X

modified theorem power_series.coeff_trunc

modified theorem power_series.coeff_zero_C

modified theorem power_series.coeff_zero_X

modified theorem power_series.coeff_zero_eq_constant_coeff_apply

modified theorem power_series.coeff_zero_mul_X

modified theorem power_series.coeff_zero_one

modified def power_series.constant_coeff

modified theorem power_series.constant_coeff_C

modified theorem power_series.constant_coeff_X

modified theorem power_series.constant_coeff_inv

modified theorem power_series.constant_coeff_inv_of_unit

modified theorem power_series.constant_coeff_one

modified theorem power_series.constant_coeff_zero

modified theorem power_series.eq_zero_or_eq_zero_of_mul_eq_zero

modified theorem power_series.ext

modified theorem power_series.ext_iff

modified theorem power_series.inv_eq_inv_aux

modified theorem power_series.inv_eq_zero

modified def power_series.inv_of_unit

modified theorem power_series.inv_of_unit_eq'

modified theorem power_series.inv_of_unit_eq

modified theorem power_series.is_unit_constant_coeff

modified theorem power_series.le_order

modified theorem power_series.le_order_add

modified def power_series.map

modified theorem power_series.map_id

modified def power_series.mk

modified def power_series.monomial

modified theorem power_series.monomial_eq_mk

modified theorem power_series.monomial_zero_eq_C

modified theorem power_series.monomial_zero_eq_C_apply

modified theorem power_series.mul_inv_of_unit

modified theorem power_series.nat_le_order

modified def power_series.order

modified theorem power_series.order_X

modified theorem power_series.order_X_pow

modified theorem power_series.order_add_of_order_eq

modified theorem power_series.order_eq

modified theorem power_series.order_eq_nat

modified theorem power_series.order_eq_top

modified theorem power_series.order_finite_of_coeff_ne_zero

modified theorem power_series.order_le

modified theorem power_series.order_monomial

modified theorem power_series.order_monomial_of_ne_zero

modified theorem power_series.order_mul

modified theorem power_series.order_mul_ge

modified theorem power_series.order_one

modified theorem power_series.order_zero

modified theorem power_series.span_X_is_prime

modified def power_series.trunc

modified theorem power_series.trunc_C

modified theorem power_series.trunc_add

modified theorem power_series.trunc_one

modified theorem power_series.trunc_zero

modified def power_series