Commit 2022-04-25 06:24 962bfcdb

View on Github →

chore(field_theory/finite/polynomial): tidy + remove nolints (#13645) Some of these definitions only make full sense over a field (for example the indicator function can be nonsensical in non-field rings) but there's also no reason not to define them more generally. This removes all nolints related to this file, and all of the generalisation linter suggestions too.

Estimated changes

Modified src/field_theory/finite/polynomial.lean

modified def mv_polynomial.R

modified theorem mv_polynomial.dim_R

modified theorem mv_polynomial.eq_zero_of_eval_eq_zero

modified def mv_polynomial.evalᵢ

modified def mv_polynomial.evalₗ

deleted theorem mv_polynomial.evalₗ_apply

modified theorem mv_polynomial.expand_zmod

modified theorem mv_polynomial.finrank_R

modified theorem mv_polynomial.frobenius_zmod

modified def mv_polynomial.indicator

modified theorem mv_polynomial.ker_evalₗ

modified theorem mv_polynomial.range_evalᵢ