[Merged by Bors] - 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

Closed

FMLJohn wants to merge 18 commits intomasterfrom hilbert

+147-3

Commits on Nov 20, 2024

Commits on Nov 21, 2024

lake exe shake --update
FMLJohn
committed

Commits on Nov 23, 2024

omitted some variables
FMLJohn
committed

Commits on Nov 26, 2024

Commits on Nov 28, 2024

generalised to arbitrary fields F with char(F) = 0
FMLJohn
committed

Commits on Dec 1, 2024

Commits on Dec 2, 2024