Theorem Polynomial.hilbertPoly_zero_nat

Modification history

2024-12-20 08:07
Mathlib/RingTheory/Polynomial/HilbertPoly.lean
feat(RingTheory/Polynomial/HilbertPoly): `Polynomial.hilbertPoly_linearMap` (#19897)
Deleted Polynomial.hilbertPoly_zero_natView on Github →
2024-12-02 18:04
Mathlib/RingTheory/Polynomial/HilbertPoly.lean
feat(RingTheory/Polynomial/HilbertPoly): the definition and key property of `Polynomial.hilbertPoly p d` for `p : F[X]` and `d : ℕ`, where `F` is a field. (#19303) …
Added Polynomial.hilbertPoly_zero_natView on Github →