Commit 2023-03-15 08:33 ac78b1da

View on Github →

feat: port Data.MvPolynomial.Basic (#2861)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Basic.lean

added theorem Algebra.adjoin_eq_range

added theorem Algebra.adjoin_range_eq_range_aeval

added def MvPolynomial.C

added theorem MvPolynomial.C_0

added theorem MvPolynomial.C_1

added theorem MvPolynomial.C_add

added theorem MvPolynomial.C_apply

added theorem MvPolynomial.C_dvd_iff_dvd_coeff

added theorem MvPolynomial.C_dvd_iff_map_hom_eq_zero

added theorem MvPolynomial.C_eq_coe_nat

added theorem MvPolynomial.C_eq_smul_one

added theorem MvPolynomial.C_inj

added theorem MvPolynomial.C_injective

added theorem MvPolynomial.C_mul'

added theorem MvPolynomial.C_mul

added theorem MvPolynomial.C_mul_X_eq_monomial

added theorem MvPolynomial.C_mul_X_pow_eq_monomial

added theorem MvPolynomial.C_mul_monomial

added theorem MvPolynomial.C_pow

added theorem MvPolynomial.C_surjective

added def MvPolynomial.X

added theorem MvPolynomial.X_inj

added theorem MvPolynomial.X_injective

added theorem MvPolynomial.X_pow_eq_monomial

added theorem MvPolynomial.adjoin_range_X

added def MvPolynomial.aeval

added def MvPolynomial.aevalTower

added theorem MvPolynomial.aevalTower_C

added theorem MvPolynomial.aevalTower_X

added theorem MvPolynomial.aevalTower_algebraMap

added theorem MvPolynomial.aevalTower_comp_C

added theorem MvPolynomial.aevalTower_comp_algebraMap

added theorem MvPolynomial.aevalTower_comp_toAlgHom

added theorem MvPolynomial.aevalTower_id

added theorem MvPolynomial.aevalTower_ofId

added theorem MvPolynomial.aevalTower_toAlgHom

added theorem MvPolynomial.aeval_C

added theorem MvPolynomial.aeval_X

added theorem MvPolynomial.aeval_X_left

added theorem MvPolynomial.aeval_X_left_apply

added theorem MvPolynomial.aeval_def

added theorem MvPolynomial.aeval_eq_eval₂Hom

added theorem MvPolynomial.aeval_eq_zero

added theorem MvPolynomial.aeval_monomial

added theorem MvPolynomial.aeval_prod

added theorem MvPolynomial.aeval_sum

added theorem MvPolynomial.aeval_unique

added theorem MvPolynomial.aeval_zero'

added theorem MvPolynomial.aeval_zero

added theorem MvPolynomial.algHom_C

added theorem MvPolynomial.algHom_ext'

added theorem MvPolynomial.algHom_ext

added theorem MvPolynomial.algebraMap_eq

added theorem MvPolynomial.as_sum

added theorem MvPolynomial.coe_eval₂Hom

added def MvPolynomial.coeff

added def MvPolynomial.coeffAddMonoidHom

added theorem MvPolynomial.coeff_C

added theorem MvPolynomial.coeff_C_mul

added theorem MvPolynomial.coeff_X'

added theorem MvPolynomial.coeff_X

added theorem MvPolynomial.coeff_X_mul'

added theorem MvPolynomial.coeff_X_mul

added theorem MvPolynomial.coeff_X_pow

added theorem MvPolynomial.coeff_add

added theorem MvPolynomial.coeff_map

added theorem MvPolynomial.coeff_monomial

added theorem MvPolynomial.coeff_monomial_mul'

added theorem MvPolynomial.coeff_monomial_mul

added theorem MvPolynomial.coeff_mul

added theorem MvPolynomial.coeff_mul_X'

added theorem MvPolynomial.coeff_mul_X

added theorem MvPolynomial.coeff_mul_monomial'

added theorem MvPolynomial.coeff_mul_monomial

added theorem MvPolynomial.coeff_one

added theorem MvPolynomial.coeff_smul

added theorem MvPolynomial.coeff_sum

added theorem MvPolynomial.coeff_zero

added theorem MvPolynomial.coeff_zero_C

added theorem MvPolynomial.coeff_zero_X

added theorem MvPolynomial.coeff_zero_one

added theorem MvPolynomial.comp_aeval

added theorem MvPolynomial.comp_eval₂Hom

added def MvPolynomial.constantCoeff

added theorem MvPolynomial.constantCoeff_C

added theorem MvPolynomial.constantCoeff_X

added theorem MvPolynomial.constantCoeff_comp_C

added theorem MvPolynomial.constantCoeff_comp_algebraMap

added theorem MvPolynomial.constantCoeff_comp_map

added theorem MvPolynomial.constantCoeff_eq

added theorem MvPolynomial.constantCoeff_map

added theorem MvPolynomial.constantCoeff_monomial

added theorem MvPolynomial.constantCoeff_smul

added theorem MvPolynomial.eq_zero_iff

added def MvPolynomial.eval

added theorem MvPolynomial.eval_C

added theorem MvPolynomial.eval_X

added theorem MvPolynomial.eval_assoc

added theorem MvPolynomial.eval_eq'

added theorem MvPolynomial.eval_eq

added theorem MvPolynomial.eval_map

added theorem MvPolynomial.eval_monomial

added theorem MvPolynomial.eval_prod

added theorem MvPolynomial.eval_sum

added theorem MvPolynomial.eval_zero'

added theorem MvPolynomial.eval_zero

added def MvPolynomial.eval₂

added def MvPolynomial.eval₂Hom

added theorem MvPolynomial.eval₂Hom_C

added theorem MvPolynomial.eval₂Hom_X'

added theorem MvPolynomial.eval₂Hom_congr

added theorem MvPolynomial.eval₂Hom_eq_zero

added theorem MvPolynomial.eval₂Hom_map_hom

added theorem MvPolynomial.eval₂Hom_monomial

added theorem MvPolynomial.eval₂Hom_zero'

added theorem MvPolynomial.eval₂Hom_zero'_apply

added theorem MvPolynomial.eval₂Hom_zero

added theorem MvPolynomial.eval₂Hom_zero_apply

added theorem MvPolynomial.eval₂_C

added theorem MvPolynomial.eval₂_X

added theorem MvPolynomial.eval₂_add

added theorem MvPolynomial.eval₂_assoc

added theorem MvPolynomial.eval₂_comp_left

added theorem MvPolynomial.eval₂_comp_right

added theorem MvPolynomial.eval₂_congr

added theorem MvPolynomial.eval₂_eq'

added theorem MvPolynomial.eval₂_eq

added theorem MvPolynomial.eval₂_eq_eval_map

added theorem MvPolynomial.eval₂_eta

added theorem MvPolynomial.eval₂_map

added theorem MvPolynomial.eval₂_monomial

added theorem MvPolynomial.eval₂_mul

added theorem MvPolynomial.eval₂_mul_C

added theorem MvPolynomial.eval₂_mul_monomial

added theorem MvPolynomial.eval₂_one

added theorem MvPolynomial.eval₂_pow

added theorem MvPolynomial.eval₂_prod

added theorem MvPolynomial.eval₂_sum

added theorem MvPolynomial.eval₂_zero'_apply

added theorem MvPolynomial.eval₂_zero

added theorem MvPolynomial.eval₂_zero_apply

added theorem MvPolynomial.exists_coeff_ne_zero

added theorem MvPolynomial.ext

added theorem MvPolynomial.ext_iff

added theorem MvPolynomial.finsupp_support_eq_support

added theorem MvPolynomial.hom_eq_hom

added theorem MvPolynomial.induction_on'''

added theorem MvPolynomial.induction_on''

added theorem MvPolynomial.induction_on'

added theorem MvPolynomial.induction_on

added theorem MvPolynomial.induction_on_monomial

added theorem MvPolynomial.is_id

added theorem MvPolynomial.linearMap_ext

added def MvPolynomial.map

added def MvPolynomial.mapAlgHom

added theorem MvPolynomial.mapAlgHom_coe_ringHom

added theorem MvPolynomial.mapAlgHom_id

added theorem MvPolynomial.map_C

added theorem MvPolynomial.map_X

added theorem MvPolynomial.map_aeval

added theorem MvPolynomial.map_eval₂

added theorem MvPolynomial.map_eval₂Hom

added theorem MvPolynomial.map_id

added theorem MvPolynomial.map_injective

added theorem MvPolynomial.map_leftInverse

added theorem MvPolynomial.map_map

added theorem MvPolynomial.map_mapRange_eq_iff

added theorem MvPolynomial.map_monomial

added theorem MvPolynomial.map_rightInverse

added theorem MvPolynomial.map_surjective

added theorem MvPolynomial.mem_support_iff

added theorem MvPolynomial.monic_monomial_eq

added def MvPolynomial.monomial

added def MvPolynomial.monomialOneHom

added theorem MvPolynomial.monomialOneHom_apply

added theorem MvPolynomial.monomial_add_single

added theorem MvPolynomial.monomial_eq

added theorem MvPolynomial.monomial_eq_monomial_iff

added theorem MvPolynomial.monomial_eq_zero

added theorem MvPolynomial.monomial_finsupp_sum_index

added theorem MvPolynomial.monomial_left_inj

added theorem MvPolynomial.monomial_left_injective

added theorem MvPolynomial.monomial_mul

added theorem MvPolynomial.monomial_pow

added theorem MvPolynomial.monomial_single_add

added theorem MvPolynomial.monomial_sum_index

added theorem MvPolynomial.monomial_sum_one

added theorem MvPolynomial.monomial_zero'

added theorem MvPolynomial.monomial_zero

added theorem MvPolynomial.mul_def

added theorem MvPolynomial.ne_zero_iff

added theorem MvPolynomial.not_mem_support_iff

added theorem MvPolynomial.ringHom_ext'

added theorem MvPolynomial.ringHom_ext

added theorem MvPolynomial.single_eq_monomial

added theorem MvPolynomial.smul_eq_C_mul

added theorem MvPolynomial.smul_eval

added theorem MvPolynomial.sum_C

added theorem MvPolynomial.sum_def

added theorem MvPolynomial.sum_monomial_eq

added def MvPolynomial.support

added theorem MvPolynomial.support_X

added theorem MvPolynomial.support_X_mul

added theorem MvPolynomial.support_X_pow

added theorem MvPolynomial.support_add

added theorem MvPolynomial.support_map_of_injective

added theorem MvPolynomial.support_map_subset

added theorem MvPolynomial.support_monomial

added theorem MvPolynomial.support_monomial_subset

added theorem MvPolynomial.support_mul

added theorem MvPolynomial.support_mul_X

added theorem MvPolynomial.support_sdiff_support_subset_support_add

added theorem MvPolynomial.support_smul

added theorem MvPolynomial.support_sum

added theorem MvPolynomial.support_sum_monomial_coeff

added theorem MvPolynomial.support_symmDiff_support_subset_support_add

added theorem MvPolynomial.support_zero

added def MvPolynomial