Theorem Polynomial.hilbertPoly_add_left

Modification history

2024-12-20 08:07

Mathlib/RingTheory/Polynomial/HilbertPoly.lean

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

Added Polynomial.hilbertPoly_add_left View on Github →