Theorem Polynomial.hilbertPoly_smul

Modification history

2024-12-20 08:07

Mathlib/RingTheory/Polynomial/HilbertPoly.lean

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

Added Polynomial.hilbertPoly_smul View on Github →