Theorem Polynomial.exists_unique_hilbertPoly

Modification history

2024-12-18 19:47

Mathlib/RingTheory/Polynomial/HilbertPoly.lean

chore(Logic/ExistsUnique): amend usages of existsUnique to follow naming convention (#20028) …

Deleted Polynomial.exists_unique_hilbertPoly View on Github →

2024-12-04 20:23

Mathlib/RingTheory/Polynomial/HilbertPoly.lean

feat(RingTheory/Polynomial/Hilbert): `Polynomial.exists_unique_hilbertPoly` and `Polynomial.hilbertPoly_mul_one_sub_pow_add` (#19404)

Added Polynomial.exists_unique_hilbertPoly View on Github →