Commit 2025-07-15 13:39 efb60912

View on Github →

feat(Algebra/Polynomial/AlgebraMap): add lemmas (#26666)

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.coeff_zero_of_isScalarTower

added def Polynomial.mapAlg

added theorem Polynomial.mapAlg_comp

added theorem Polynomial.mapAlg_eq_map

Modified Mathlib/Algebra/Polynomial/Lifts.lean

deleted def Polynomial.mapAlg

deleted theorem Polynomial.mapAlg_eq_map