@[implicit_reducible]

noncomputable instance Finsupp.fintypeDegreeEq (n d : ℕ) : Fintype ↑{s : Fin n →₀ ℕ | degree s = d}

Finiteness instance: monomials in n variables of total degree d form a finite set.

noncomputable def degreeEquivSym (n d : ℕ) : ↑{s : Fin n →₀ ℕ | Finsupp.degree s = d} ≃ Sym (Fin n) d

Equivalence between degree-d monomials in n variables and d-element multisets in Fin n.

theorem card_degree_eq_choose (n d : ℕ) : Fintype.card ↑{s : Fin n →₀ ℕ | Finsupp.degree s = d} = (n + d - 1).choose d

The number of degree-d monomials in n variables is C(n + d - 1, d) (multiset coefficient).

theorem homogeneousSubmodule_finiteDimensional (k : Type u_1) [Field k] (n d : ℕ) : Module.Finite k ↥(MvPolynomial.homogeneousSubmodule (Fin n) k d)

The space of degree-d homogeneous polynomials in n variables over a field is finite-dimensional.

theorem homogeneousSubmodule_finrank_eq_card (k : Type u_1) [Field k] (n d : ℕ) : Module.finrank k ↥(MvPolynomial.homogeneousSubmodule (Fin n) k d) = Fintype.card ↑{s : Fin n →₀ ℕ | Finsupp.degree s = d}

The dimension of degree-d homogeneous polynomials equals the number of degree-d monomials.

theorem homogeneousSubmodule_finrank (k : Type u_1) [Field k] (n d : ℕ) : Module.finrank k ↥(MvPolynomial.homogeneousSubmodule (Fin n) k d) = (n + d - 1).choose d

Dimension of the space of degree-d forms in n variables is C(n + d - 1, d).

noncomputable def hilbertFun (k : Type u_1) [Field k] (n d : ℕ) : ℕ

The Hilbert function of P^n_k: dimension of degree-d forms in n + 1 variables.

theorem hilbert_fun_eq_choose (k : Type u_1) [Field k] (n d : ℕ) : hilbertFun k n d = (n + d).choose n

Closed form: H_{P^n}(d) = C(n + d, n).

noncomputable def hilbertFunQuotient (k : Type u_1) [Field k] (n : ℕ) (I : Ideal (MvPolynomial (Fin (n + 1)) k)) (d : ℕ) : ℕ

Hilbert function of a quotient ring: dimension of the degree-d part of k[x_0, ..., x_n] / I.

theorem hilbert_fun_is_polynomial (k : Type u_1) [Field k] (n : ℕ) : ∃ (p : Polynomial ℚ), (∀ (d : ℕ), ↑(hilbertFun k n d) = Polynomial.eval (↑d) p) ∧ p.natDegree = n

The Hilbert function of P^n is polynomial of degree exactly n.

theorem hilbert_polynomial_degree (n : ℕ) : (Polynomial.preHilbertPoly ℚ n 0).natDegree = n

The Hilbert polynomial of P^n has degree n.

theorem hilbert_polynomial_leading_coeff (n : ℕ) : (Polynomial.preHilbertPoly ℚ n 0).leadingCoeff = (↑n.factorial)⁻¹

The leading coefficient of the Hilbert polynomial of P^n is 1/n!.

theorem hilbert_fun_mono (k : Type u_1) [Field k] (n d : ℕ) : hilbertFun k n d ≤ hilbertFun k n (d + 1)

The Hilbert function of P^n is monotonically nondecreasing in d.