Commit 2023-03-13 07:16 6f2b42f1

View on Github →

feat: port Data.Polynomial.AlgebraMap (#2822)

depends on: #2817

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/AlgebraMap.lean

added theorem Algebra.adjoin_singleton_eq_range_aeval

added theorem Polynomial.C_eq_algebraMap

added theorem Polynomial.adjoin_X

added def Polynomial.aeval

added def Polynomial.aevalTower

added theorem Polynomial.aevalTower_C

added theorem Polynomial.aevalTower_X

added theorem Polynomial.aevalTower_algebraMap

added theorem Polynomial.aevalTower_comp_C

added theorem Polynomial.aevalTower_comp_algebraMap

added theorem Polynomial.aevalTower_comp_toAlgHom

added theorem Polynomial.aevalTower_id

added theorem Polynomial.aevalTower_ofId

added theorem Polynomial.aevalTower_toAlgHom

added theorem Polynomial.aeval_C

added theorem Polynomial.aeval_X

added theorem Polynomial.aeval_X_left

added theorem Polynomial.aeval_X_left_apply

added theorem Polynomial.aeval_X_pow

added theorem Polynomial.aeval_add

added theorem Polynomial.aeval_algEquiv

added theorem Polynomial.aeval_algHom

added theorem Polynomial.aeval_algHom_apply

added theorem Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval

added theorem Polynomial.aeval_bit0

added theorem Polynomial.aeval_bit1

added theorem Polynomial.aeval_comp

added theorem Polynomial.aeval_def

added theorem Polynomial.aeval_endomorphism

added theorem Polynomial.aeval_eq_sum_range'

added theorem Polynomial.aeval_eq_sum_range

added theorem Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero

added theorem Polynomial.aeval_fn_apply

added theorem Polynomial.aeval_monomial

added theorem Polynomial.aeval_mul

added theorem Polynomial.aeval_nat_cast

added theorem Polynomial.aeval_one

added theorem Polynomial.aeval_subalgebra_coe

added theorem Polynomial.aeval_zero

added theorem Polynomial.algHom_eval₂_algebraMap

added theorem Polynomial.algHom_ext'

added theorem Polynomial.algHom_ext

added theorem Polynomial.algebraMap_apply

added theorem Polynomial.coe_aeval_eq_eval

added theorem Polynomial.coe_aeval_eq_evalRingHom

added theorem Polynomial.coeff_zero_eq_aeval_zero'

added theorem Polynomial.coeff_zero_eq_aeval_zero

added theorem Polynomial.dvd_term_of_dvd_eval_of_dvd_terms

added theorem Polynomial.dvd_term_of_isRoot_of_dvd_terms

added theorem Polynomial.eval_mul_X_sub_C

added theorem Polynomial.eval_unique

added theorem Polynomial.eval₂_algebraMap_X

added theorem Polynomial.eval₂_int_castRingHom_X

added theorem Polynomial.isRoot_of_aeval_algebraMap_eq_zero

added theorem Polynomial.isRoot_of_eval₂_map_eq_zero

added theorem Polynomial.map_aeval_eq_aeval_map

added theorem Polynomial.not_isUnit_X_sub_C

added theorem Polynomial.ofFinsupp_algebraMap

added theorem Polynomial.ringHom_eval₂_cast_int_ringHom

added def Polynomial.toFinsuppIsoAlg

added theorem Polynomial.toFinsupp_algebraMap