Commit 2020-09-22 14:52 f2458d6f

View on Github →

chore(data/mv_polynomial): Rename variables (#4208) I renamed α to R throughout. I also changed the \sigma to σ in basic.lean, see leanprover-community/doc-gen#62

Estimated changes

Modified src/data/mv_polynomial/basic.lean

modified def mv_polynomial.C

modified theorem mv_polynomial.C_0

modified theorem mv_polynomial.C_1

modified theorem mv_polynomial.C_add

modified theorem mv_polynomial.C_eq_coe_nat

modified theorem mv_polynomial.C_mul

modified theorem mv_polynomial.C_pow

modified def mv_polynomial.X

modified theorem mv_polynomial.X_pow_eq_single

modified def mv_polynomial.aeval

modified theorem mv_polynomial.aeval_C

modified theorem mv_polynomial.aeval_def

modified theorem mv_polynomial.aeval_eq_zero

modified theorem mv_polynomial.aeval_monomial

modified theorem mv_polynomial.alg_hom_C

modified theorem mv_polynomial.alg_hom_ext

modified theorem mv_polynomial.algebra_map_eq

modified theorem mv_polynomial.as_sum

modified theorem mv_polynomial.coe_eval₂_hom

modified def mv_polynomial.coeff

modified theorem mv_polynomial.coeff_C_mul

modified theorem mv_polynomial.coeff_add

modified def mv_polynomial.coeff_coe_to_fun

modified theorem mv_polynomial.coeff_map

modified theorem mv_polynomial.coeff_mul

modified theorem mv_polynomial.coeff_mul_X'

modified theorem mv_polynomial.coeff_mul_X

modified theorem mv_polynomial.coeff_sum

modified theorem mv_polynomial.coeff_zero_X

modified theorem mv_polynomial.comp_eval₂_hom

modified def mv_polynomial.constant_coeff

modified theorem mv_polynomial.constant_coeff_C

modified theorem mv_polynomial.constant_coeff_comp_map

modified theorem mv_polynomial.constant_coeff_eq

modified theorem mv_polynomial.constant_coeff_map

modified theorem mv_polynomial.constant_coeff_monomial

modified theorem mv_polynomial.eq_zero_iff

modified def mv_polynomial.eval

modified theorem mv_polynomial.eval_eq'

modified theorem mv_polynomial.eval_eq

modified theorem mv_polynomial.eval_map

modified theorem mv_polynomial.eval_prod

modified theorem mv_polynomial.eval_sum

modified theorem mv_polynomial.eval_unique

modified def mv_polynomial.eval₂

modified theorem mv_polynomial.eval₂_assoc

modified theorem mv_polynomial.eval₂_comp_left

modified theorem mv_polynomial.eval₂_comp_right

modified theorem mv_polynomial.eval₂_congr

modified theorem mv_polynomial.eval₂_eq'

modified theorem mv_polynomial.eval₂_eq

modified theorem mv_polynomial.eval₂_eq_eval_map

modified theorem mv_polynomial.eval₂_eta

modified def mv_polynomial.eval₂_hom

modified theorem mv_polynomial.eval₂_hom_C

modified theorem mv_polynomial.eval₂_hom_X'

modified theorem mv_polynomial.eval₂_hom_congr

modified theorem mv_polynomial.eval₂_hom_eq_zero

modified theorem mv_polynomial.eval₂_hom_map_hom

modified theorem mv_polynomial.eval₂_hom_monomial

modified theorem mv_polynomial.eval₂_map

modified theorem mv_polynomial.eval₂_one

modified theorem mv_polynomial.eval₂_pow

modified theorem mv_polynomial.eval₂_prod

modified theorem mv_polynomial.eval₂_sum

modified theorem mv_polynomial.eval₂_zero

modified theorem mv_polynomial.exists_coeff_ne_zero

modified theorem mv_polynomial.ext

modified theorem mv_polynomial.ext_iff

modified theorem mv_polynomial.hom_eq_hom

modified theorem mv_polynomial.induction_on'

modified theorem mv_polynomial.induction_on

modified theorem mv_polynomial.is_id

modified def mv_polynomial.map

modified theorem mv_polynomial.map_C

modified theorem mv_polynomial.map_X

modified theorem mv_polynomial.map_eval₂

modified theorem mv_polynomial.map_eval₂_hom

modified theorem mv_polynomial.map_id

modified theorem mv_polynomial.map_map

modified theorem mv_polynomial.map_monomial

modified theorem mv_polynomial.monic_monomial_eq

modified def mv_polynomial.monomial

modified theorem mv_polynomial.monomial_add

modified theorem mv_polynomial.monomial_eq

modified theorem mv_polynomial.monomial_mul

modified theorem mv_polynomial.monomial_zero

modified theorem mv_polynomial.ne_zero_iff

modified theorem mv_polynomial.ring_hom_ext

modified theorem mv_polynomial.single_eq_C_mul_X

modified theorem mv_polynomial.smul_eq_C_mul

modified theorem mv_polynomial.smul_eval

modified theorem mv_polynomial.support_map_of_injective

modified theorem mv_polynomial.support_map_subset

modified theorem mv_polynomial.support_sum_monomial_coeff

modified def mv_polynomial

Modified src/data/mv_polynomial/comm_ring.lean

modified theorem mv_polynomial.C_neg

modified theorem mv_polynomial.C_sub

modified theorem mv_polynomial.coeff_neg

modified theorem mv_polynomial.coeff_sub

modified theorem mv_polynomial.degrees_neg

modified theorem mv_polynomial.degrees_sub

modified theorem mv_polynomial.eval₂_hom_X

modified theorem mv_polynomial.hom_C

modified def mv_polynomial.hom_equiv

modified theorem mv_polynomial.total_degree_neg

modified theorem mv_polynomial.total_degree_sub

Modified src/data/mv_polynomial/equiv.lean

modified def mv_polynomial.iter_to_sum

modified theorem mv_polynomial.iter_to_sum_C_C

modified theorem mv_polynomial.iter_to_sum_C_X

modified theorem mv_polynomial.iter_to_sum_X

modified def mv_polynomial.mv_polynomial_equiv_mv_polynomial

modified def mv_polynomial.option_equiv_left

modified def mv_polynomial.option_equiv_right

modified def mv_polynomial.pempty_ring_equiv

modified def mv_polynomial.punit_ring_equiv

modified def mv_polynomial.ring_equiv_congr

modified def mv_polynomial.ring_equiv_of_equiv

modified def mv_polynomial.sum_ring_equiv

modified def mv_polynomial.sum_to_iter

modified theorem mv_polynomial.sum_to_iter_C

modified theorem mv_polynomial.sum_to_iter_Xl

modified theorem mv_polynomial.sum_to_iter_Xr

Modified src/data/mv_polynomial/monad.lean

Modified src/data/mv_polynomial/variables.lean

modified theorem mv_polynomial.aeval_eq_constant_coeff_of_vars

modified theorem mv_polynomial.coeff_eq_zero_of_total_degree_lt

modified def mv_polynomial.degree_of

modified def mv_polynomial.degrees

modified theorem mv_polynomial.degrees_C

modified theorem mv_polynomial.degrees_X

modified theorem mv_polynomial.degrees_add

modified theorem mv_polynomial.degrees_add_of_disjoint

modified theorem mv_polynomial.degrees_map

modified theorem mv_polynomial.degrees_map_of_injective

modified theorem mv_polynomial.degrees_monomial

modified theorem mv_polynomial.degrees_monomial_eq

modified theorem mv_polynomial.degrees_mul

modified theorem mv_polynomial.degrees_one

modified theorem mv_polynomial.degrees_pow

modified theorem mv_polynomial.degrees_prod

modified theorem mv_polynomial.degrees_sum

modified theorem mv_polynomial.degrees_zero

modified theorem mv_polynomial.eval₂_hom_eq_constant_coeff_of_vars

modified theorem mv_polynomial.exists_degree_lt

modified theorem mv_polynomial.le_degrees_add

modified theorem mv_polynomial.mem_degrees

modified theorem mv_polynomial.mem_support_not_mem_vars_zero

modified def mv_polynomial.total_degree

modified theorem mv_polynomial.total_degree_C

modified theorem mv_polynomial.total_degree_X

modified theorem mv_polynomial.total_degree_add

modified theorem mv_polynomial.total_degree_eq

modified theorem mv_polynomial.total_degree_le_degrees_card

modified theorem mv_polynomial.total_degree_mul

modified theorem mv_polynomial.total_degree_multiset_prod

modified theorem mv_polynomial.total_degree_one

modified theorem mv_polynomial.total_degree_pow

modified theorem mv_polynomial.total_degree_zero

modified def mv_polynomial.vars

modified theorem mv_polynomial.vars_0

modified theorem mv_polynomial.vars_C

modified theorem mv_polynomial.vars_X

modified theorem mv_polynomial.vars_add_subset

modified theorem mv_polynomial.vars_monomial_single

modified theorem mv_polynomial.vars_mul

modified theorem mv_polynomial.vars_one

modified theorem mv_polynomial.vars_pow

modified theorem mv_polynomial.vars_prod