Commit 2025-01-13 17:41 8c3ecf43

View on Github →

chore(Algebra/MvPolynomial/Eval): split file for eval off of basic (#20655) This PR directly splits Algebra/MvPolynomial/Basic at the point where eval related functions are defined. This addresses an instance of a file over 1500 lines long, and makes the MvPolynomial/ directory structure slightly more like Polynomial/.

Estimated changes

deleted theorem Algebra.adjoin_eq_range
deleted def MvPolynomial.aeval
deleted theorem MvPolynomial.aevalTower_C
deleted theorem MvPolynomial.aevalTower_X
deleted theorem MvPolynomial.aeval_C
deleted theorem MvPolynomial.aeval_X
deleted theorem MvPolynomial.aeval_X_left
deleted theorem MvPolynomial.aeval_def
deleted theorem MvPolynomial.aeval_ofNat
deleted theorem MvPolynomial.aeval_prod
deleted theorem MvPolynomial.aeval_sum
deleted theorem MvPolynomial.aeval_unique
deleted theorem MvPolynomial.aeval_zero'
deleted theorem MvPolynomial.aeval_zero
deleted theorem MvPolynomial.coeff_map
deleted theorem MvPolynomial.comp_aeval
deleted def MvPolynomial.eval
deleted theorem MvPolynomial.eval_C
deleted theorem MvPolynomial.eval_X
deleted theorem MvPolynomial.eval_add
deleted theorem MvPolynomial.eval_assoc
deleted theorem MvPolynomial.eval_eq'
deleted theorem MvPolynomial.eval_eq
deleted theorem MvPolynomial.eval_eval₂
deleted theorem MvPolynomial.eval_map
deleted theorem MvPolynomial.eval_mem
deleted theorem MvPolynomial.eval_mul
deleted theorem MvPolynomial.eval_ofNat
deleted theorem MvPolynomial.eval_pow
deleted theorem MvPolynomial.eval_prod
deleted theorem MvPolynomial.eval_sum
deleted theorem MvPolynomial.eval_zero'
deleted theorem MvPolynomial.eval_zero
deleted theorem MvPolynomial.eval₂Hom_C
deleted theorem MvPolynomial.eval₂_C
deleted theorem MvPolynomial.eval₂_X
deleted theorem MvPolynomial.eval₂_add
deleted theorem MvPolynomial.eval₂_comp
deleted theorem MvPolynomial.eval₂_eq'
deleted theorem MvPolynomial.eval₂_eq
deleted theorem MvPolynomial.eval₂_eta
deleted theorem MvPolynomial.eval₂_id
deleted theorem MvPolynomial.eval₂_map
deleted theorem MvPolynomial.eval₂_mem
deleted theorem MvPolynomial.eval₂_mul
deleted theorem MvPolynomial.eval₂_one
deleted theorem MvPolynomial.eval₂_pow
deleted theorem MvPolynomial.eval₂_prod
deleted theorem MvPolynomial.eval₂_sum
deleted theorem MvPolynomial.eval₂_zero
deleted def MvPolynomial.map
deleted theorem MvPolynomial.mapAlgHom_id
deleted theorem MvPolynomial.map_C
deleted theorem MvPolynomial.map_X
deleted theorem MvPolynomial.map_aeval
deleted theorem MvPolynomial.map_eval₂
deleted theorem MvPolynomial.map_id
deleted theorem MvPolynomial.map_map
deleted theorem MvPolynomial.map_monomial
deleted theorem MvPolynomial.smul_eval
added theorem MvPolynomial.aeval_C
added theorem MvPolynomial.aeval_X
added theorem MvPolynomial.aeval_def
added theorem MvPolynomial.aeval_sum
added theorem MvPolynomial.coeff_map
added theorem MvPolynomial.eval_C
added theorem MvPolynomial.eval_X
added theorem MvPolynomial.eval_add
added theorem MvPolynomial.eval_eq'
added theorem MvPolynomial.eval_eq
added theorem MvPolynomial.eval_map
added theorem MvPolynomial.eval_mem
added theorem MvPolynomial.eval_mul
added theorem MvPolynomial.eval_pow
added theorem MvPolynomial.eval_prod
added theorem MvPolynomial.eval_sum
added theorem MvPolynomial.eval_zero
added theorem MvPolynomial.eval₂_C
added theorem MvPolynomial.eval₂_X
added def MvPolynomial.map
added theorem MvPolynomial.map_C
added theorem MvPolynomial.map_X
added theorem MvPolynomial.map_aeval
added theorem MvPolynomial.map_id
added theorem MvPolynomial.map_map
added theorem MvPolynomial.smul_eval