Commit 2024-12-20 08:07 e0cf109c

View on Github →

feat(RingTheory/Polynomial/HilbertPoly): Polynomial.hilbertPoly_linearMap (#19897)

Estimated changes

Modified Mathlib/RingTheory/Polynomial/HilbertPoly.lean

added theorem Polynomial.hilbertPoly_add_left

deleted theorem Polynomial.hilbertPoly_poly_succ

deleted theorem Polynomial.hilbertPoly_poly_zero

added theorem Polynomial.hilbertPoly_smul

added theorem Polynomial.hilbertPoly_succ

added theorem Polynomial.hilbertPoly_zero_left

deleted theorem Polynomial.hilbertPoly_zero_nat

added theorem Polynomial.hilbertPoly_zero_right