Commit 2025-01-28 07:05 8be3c373

View on Github →

feat(Algebra/Polynomial): Polynomial.aeval for product algebras (#21062) Results about evaluating polynomials on elements from (generalized) product algebras. Add necessary (and basic) facts for Pi algebras.

Estimated changes

Modified Mathlib/Algebra/Algebra/Pi.lean

added theorem Pi.algHom_comp

added theorem Pi.algHom_evalAlgHom

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.aeval_pi

added theorem Polynomial.aeval_pi_apply

added theorem Polynomial.aeval_pi_apply₂

added theorem Polynomial.aeval_prod

added theorem Polynomial.aeval_prod_apply