Commit 2023-11-10 09:14 48b0f038

View on Github →

feat(Data/Polynomial/AlgebraMap): more results for non-commutative polynomials (#8116) This adds an AlgHom version of eval₂RingHom', and a stronger ext lemma for noncommutative algebras. This is a follow-up to leanprover-community/mathlib#9250 This better ext lemma golfs away most of a nasty proof.

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

added theorem Matrix.map_id'

Modified Mathlib/Data/Polynomial/AlgebraMap.lean

added def Polynomial.CAlgHom

modified theorem Polynomial.algHom_ext'

modified theorem Polynomial.algHom_ext

added def Polynomial.eval₂AlgHom'

Modified Mathlib/Data/Polynomial/Eval.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

added theorem Matrix.matPolyEquiv_eval_eq_map

added theorem Matrix.matPolyEquiv_symm_map_eval

Modified Mathlib/RingTheory/Localization/Integral.lean

Modified Mathlib/RingTheory/PowerBasis.lean