Multiplication.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.symMonomialRaw_append line 14

Source documentation

Concatenating two lists of factors multiplies their symmetric monomials.

theorem symMonomialRaw_append (m n : ℕ) (v : Fin m → V) (w : Fin n → V) :
    symMonomialRaw (m + n) V (Fin.append v w) =
      symMonomialRaw m V v * symMonomialRaw n V w := by
…

Mentions: OAI.Problem346.symMonomialRaw

theorem OAI.Problem346.symPowSubmodule_mul line 20
Source documentation
Products of homogeneous spans have the sum of their degrees.
```
theorem symPowSubmodule_mul (m n : ℕ) :
    symPowSubmodule m V * symPowSubmodule n V = symPowSubmodule (m + n) V := by
…
```
Mentions: OAI.Problem346.symPowSubmodule
theorem OAI.Problem346.symPow_mul_mem line 35
Source documentation
The product of two elements of the indicated homogeneous pieces.
```
theorem symPow_mul_mem (m n : ℕ) (x : SymPow m V) (y : SymPow n V) :
    (x : SymmetricAlgebra ℂ V) * (y : SymmetricAlgebra ℂ V) ∈
      symPowSubmodule (m+n) V := by
…
```
Mentions: OAI.Problem346.SymPow, OAI.Problem346.symPowSubmodule
def OAI.Problem346.symPowMul line 42
Source documentation
Graded multiplication in the symmetric algebra, as a bilinear map.
```
def symPowMul (m n : ℕ) :
    SymPow m V →ₗ[ℂ] SymPow n V →ₗ[ℂ] SymPow (m+n) V :=
…
```
Mentions: OAI.Problem346.SymPow
theorem OAI.Problem346.symPowMul_coe line 52
theorem OAI.Problem346.symPowMul_symMonomial line 56
def OAI.Problem346.symPowCast line 63
Source documentation
Transport a homogeneous element across an equality of degrees.
```
def symPowCast {m n : ℕ} (h : m = n) : SymPow m V ≃ₗ[ℂ] SymPow n V :=
…
```
Mentions: OAI.Problem346.SymPow
theorem OAI.Problem346.symPowCast_coe line 66
theorem OAI.Problem346.symPowCast_symMonomial line 69
def OAI.Problem346.symPowMulCast line 76
Source documentation
Multiplication followed by transport to a specified total degree.
```
def symPowMulCast (m n b : ℕ) (h : m+n=b) :
    SymPow m V →ₗ[ℂ] SymPow n V →ₗ[ℂ] SymPow b V :=
…
```
Mentions: OAI.Problem346.SymPow
theorem OAI.Problem346.symPowMulCast_coe line 81
theorem OAI.Problem346.symMonomialRaw_const line 87
Source documentation
The raw monomial of a constant tuple is a power.
```
theorem symMonomialRaw_const (n : ℕ) (v : V) :
    symMonomialRaw n V (fun _ => v) = SymmetricAlgebra.ι ℂ V v ^ n := by
…
```
Mentions: OAI.Problem346.symMonomialRaw