Commit 2023-05-21 08:56 3c517ae2

View on Github →

feat: port RingTheory.PolynomialAlgebra (#4106) This is my first attempt at porting a file. I fixed a few of the errors, but there are still two issues left.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/PolynomialAlgebra.lean

added def PolyEquivTensor.equiv

added def PolyEquivTensor.invFun

added theorem PolyEquivTensor.invFun_add

added theorem PolyEquivTensor.invFun_monomial

added theorem PolyEquivTensor.left_inv

added theorem PolyEquivTensor.right_inv

added def PolyEquivTensor.toFunAlgHom

added theorem PolyEquivTensor.toFunAlgHom_apply_tmul

added def PolyEquivTensor.toFunBilinear

added theorem PolyEquivTensor.toFunBilinear_apply_eq_sum

added def PolyEquivTensor.toFunLinear

added theorem PolyEquivTensor.toFunLinear_algebraMap_tmul_one

added theorem PolyEquivTensor.toFunLinear_mul_tmul_mul

added theorem PolyEquivTensor.toFunLinear_tmul_apply

added theorem PolyEquivTensor.to_fun_linear_mul_tmul_mul_aux_1

added theorem PolyEquivTensor.to_fun_linear_mul_tmul_mul_aux_2

added theorem matPolyEquiv_coeff_apply

added theorem matPolyEquiv_coeff_apply_aux_1

added theorem matPolyEquiv_coeff_apply_aux_2

added theorem matPolyEquiv_smul_one

added theorem matPolyEquiv_symm_apply_coeff

added def polyEquivTensor

added theorem polyEquivTensor_apply

added theorem polyEquivTensor_symm_apply_tmul

added theorem support_subset_support_matPolyEquiv