BinaryFactorization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.binary_power_factorization line 11

Source documentation

Binary forms used in the first step of the vanishing argument split into linear factors.

theorem binary_power_factorization {A : Type*} [CommRing A] [Algebra ℂ A]
    (r : ℕ) (hr : 0 < r) (x y : A) (c : ℂ) :
    ∃ z : Fin r → ℂ, (∏ i : Fin r, (x - z i • y)) = x ^ r + c • y ^ r := by
…

theorem OAI.Problem346.symMonomialRaw_binary_power line 42

Source documentation

In the symmetric algebra, a binary sum of pure powers is a product of vectors.

theorem symMonomialRaw_binary_power (V : Type*) [AddCommGroup V] [Module ℂ V]
    (r : ℕ) (hr : 0 < r) (x y : V) (c : ℂ) :
    ∃ v : Fin r → V, symMonomialRaw r V v =
      (SymmetricAlgebra.ι ℂ V x) ^ r + c • (SymmetricAlgebra.ι ℂ V y) ^ r := by
…

Mentions: OAI.Problem346.symMonomialRaw

theorem OAI.Problem346.symMonomialRaw_binary_power_mul line 52

Source documentation

Multiplying a split binary power by a product remains a product, with the exact degree.

theorem symMonomialRaw_binary_power_mul (V : Type*) [AddCommGroup V] [Module ℂ V]
    (r m : ℕ) (hr : 0 < r) (x y : V) (c : ℂ) (u : Fin m → V) :
    ∃ v : Fin (r + m) → V, symMonomialRaw (r + m) V v =
      ((SymmetricAlgebra.ι ℂ V x) ^ r + c • (SymmetricAlgebra.ι ℂ V y) ^ r) *
        symMonomialRaw m V u := by
…

Mentions: OAI.Problem346.symMonomialRaw

theorem OAI.Problem346.symMonomial_binary_power_mul line 63

Source documentation

The split binary form is a genuine product in the prescribed symmetric-power subtype.

theorem symMonomial_binary_power_mul (V : Type*) [AddCommGroup V] [Module ℂ V]
    (r m : ℕ) (hr : 0 < r) (x y : V) (c : ℂ) (u : Fin m → V) :
    ∃ v : Fin (r + m) → V, symMonomial (r + m) V v =
      symMonomial (r + m) V (Fin.append (fun _ : Fin r => x) u) +
        c • symMonomial (r + m) V (Fin.append (fun _ : Fin r => y) u) := by
…

Mentions: OAI.Problem346.symMonomial