Commit 2023-06-02 16:56 b7e84bf0

View on Github →

Port/FieldTheory.Finite.Polynomial (#4597)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Finite/Polynomial.lean

added def MvPolynomial.R

added theorem MvPolynomial.c_dvd_iff_zMod

added theorem MvPolynomial.degrees_indicator

added theorem MvPolynomial.eq_zero_of_eval_eq_zero

added theorem MvPolynomial.eval_indicator_apply_eq_one

added theorem MvPolynomial.eval_indicator_apply_eq_zero

added def MvPolynomial.evalᵢ

added def MvPolynomial.evalₗ

added theorem MvPolynomial.expand_zMod

added theorem MvPolynomial.finrank_R

added theorem MvPolynomial.frobenius_zMod

added def MvPolynomial.indicator

added theorem MvPolynomial.indicator_mem_restrictDegree

added theorem MvPolynomial.ker_evalₗ

added theorem MvPolynomial.map_restrict_dom_evalₗ

added theorem MvPolynomial.range_evalᵢ

added theorem MvPolynomial.rank_R