Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-24 17:38 e23b97e5

View on Github →

feat(ring_theory/polynomial): decomposing the kernel of an endomorphism polynomial (#4174)

Estimated changes

Modified src/algebra/ring/basic.lean

added theorem ring_hom.map_bit0

added theorem ring_hom.map_bit1

Modified src/data/polynomial/algebra_map.lean

added theorem polynomial.aeval_X_pow

added theorem polynomial.aeval_add

added theorem polynomial.aeval_bit0

added theorem polynomial.aeval_bit1

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_zero

Modified src/data/polynomial/eval.lean

deleted theorem polynomial.eval₂_endomorphism_algebra_map

Modified src/linear_algebra/basic.lean

added theorem linear_map.mul_apply

Modified src/ring_theory/algebra.lean

added theorem alg_hom.map_bit0

added theorem alg_hom.map_bit1

Modified src/ring_theory/polynomial/basic.lean

added theorem polynomial.disjoint_ker_aeval_of_coprime

added theorem polynomial.sup_aeval_range_eq_top_of_coprime

added theorem polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime

added theorem polynomial.sup_ker_aeval_le_ker_aeval_mul