FirstPolynomial.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.firstPolynomial line 17
Source documentation
The scalar polynomial at the k-th stage of the first transfer sequence.
```
def firstPolynomial {r m : ℕ}
    (T : SymmetricMultilinearForm (r+1) (r+m) V) (e : κ → V) (k : ℕ) :
    MvPolynomial (FirstBlock m × κ) ℂ :=
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.FirstBlock
theorem OAI.Problem346.firstPolynomial_blockHomogeneous line 23
Source documentation
Direct block degrees of every intermediate polynomial, by counting its labels.
```
theorem firstPolynomial_blockHomogeneous {r m : ℕ}
    (T : SymmetricMultilinearForm (r+1) (r+m) V) (e : κ → V)
    (k : ℕ) (u : FirstBlock m) :
    PolynomialWeights.IsBlockHomogeneous u (firstPolynomial T e k)
      (Finset.univ.filter (fun p => firstLabel r m k p = u)).card := by
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.FirstBlock, OAI.Problem346.PolynomialWeights.IsBlockHomogeneous, OAI.Problem346.firstPolynomial, OAI.Problem346.firstLabel