HomogeneousSpaceDimension.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.degreeExponentsEquivSym line 12
Source documentation
Degree-exact exponent vectors are multisets of the indicated cardinality.
```
def degreeExponentsEquivSym (σ : Type u) (d : ℕ) :
    { m : σ →₀ ℕ // m.degree = d } ≃ Sym σ d := by
…
```

theorem OAI.Problem335.card_degree_exponents line 18

Source documentation

The number of monomials of total degree d.

theorem card_degree_exponents (σ : Type u) [Fintype σ] (d : ℕ) :
    Nat.card { m : σ →₀ ℕ // m.degree = d } =
      Nat.multichoose (Fintype.card σ) d := by
…

instance OAI.Problem335.homogeneousSubmodule_finite line 25

Source documentation

Homogeneous polynomial spaces in finitely many variables are finite modules.

instance homogeneousSubmodule_finite (K : Type u) [CommSemiring K]
    (σ : Type v) [Finite σ] (d : ℕ) :
    Module.Finite K (MvPolynomial.homogeneousSubmodule σ K d) :=
…

theorem OAI.Problem335.homogeneousSubmodule_finrank line 31

Source documentation

Exact dimension of the homogeneous polynomial space.

theorem homogeneousSubmodule_finrank (K : Type u) [Field K]
    (σ : Type v) [Fintype σ] (d : ℕ) :
    Module.finrank K (MvPolynomial.homogeneousSubmodule σ K d) =
      Nat.multichoose (Fintype.card σ) d := by
…

theorem OAI.Problem335.homogeneousSubmodule_finrank_choose line 41

Source documentation

The usual stars-and-bars presentation of homogeneous dimension.

theorem homogeneousSubmodule_finrank_choose (K : Type u) [Field K]
    (σ : Type v) [Fintype σ] (d : ℕ) :
    Module.finrank K (MvPolynomial.homogeneousSubmodule σ K d) =
      Nat.choose (Fintype.card σ + d - 1) d := by
…

theorem OAI.Problem335.homogeneousTensor_finrank line 48

Source documentation

Dimension of the separate-variable source/intermediate spaces used by the rank measure.

theorem homogeneousTensor_finrank (K : Type u) [Field K]
    (σ : Type v) [Fintype σ] (τ : Type w) [Fintype τ] (a b : ℕ) :
    Module.finrank K (TensorProduct K
      (MvPolynomial.homogeneousSubmodule σ K a)
      (MvPolynomial.homogeneousSubmodule τ K b)) =
      Nat.choose (Fintype.card σ + a - 1) a *
      Nat.choose (Fintype.card τ + b - 1) b := by
…