Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-26 01:11 e064a7bf

View on Github →

feat(data/polynomial/div): prove that evaluation induces an isomorphism of algebras (#18480) Also prove that aeval coerces to eval_ring_hom.

Estimated changes

Modified src/data/polynomial/algebra_map.lean

modified theorem polynomial.coe_aeval_eq_eval

added theorem polynomial.coe_aeval_eq_eval_ring_hom

Modified src/data/polynomial/div.lean

added theorem polynomial.ker_eval_ring_hom

added theorem polynomial.quotient_span_X_sub_C_alg_equiv_mk

added theorem polynomial.quotient_span_X_sub_C_alg_equiv_symm_apply

Modified src/data/polynomial/eval.lean

added theorem polynomial.eval_surjective

Modified src/ring_theory/ideal/operations.lean

added def ideal.quotient_equiv_alg_of_eq

added theorem ideal.quotient_equiv_alg_of_eq_mk

added theorem ideal.quotient_equiv_alg_of_eq_symm

Modified src/ring_theory/ideal/quotient.lean