ProductNormalization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.homogeneous_zero_eq_C line 17
Source documentation
A homogeneous polynomial of formal degree zero is a scalar, including the zero polynomial.
```
theorem homogeneous_zero_eq_C {p : MvPolynomial σ K}
    (hp : p.IsHomogeneous 0) : p = C (constantCoeff p) := by
…
```

theorem OAI.Problem335.homogeneous_product_positive_factors line 25

Source documentation

Remove formal-degree-zero factors from a homogeneous product and absorb them into a single scalar. Positive-degree occurrences, including repeated occurrences and zero polynomials, are retained.

theorem homogeneous_product_positive_factors
    (l : List (MvPolynomial σ K × ℕ))
    (hl : ∀ q ∈ l, q.1.IsHomogeneous q.2) :
    ∃ a : K, ∃ factors : List (MvPolynomial σ K × ℕ),
      (∀ q ∈ factors, 0 < q.2 ∧ q.1.IsHomogeneous q.2) ∧
      (factors.map Prod.snd).sum = (l.map Prod.snd).sum ∧
      (l.map Prod.fst).prod = C a * (factors.map Prod.fst).prod ∧
      factors.Sublist l ∧
      factors.length ≤ (l.map Prod.snd).sum := by
…

theorem OAI.Problem335.homogeneous_product_linear_factors line 68

Source documentation

When the original formal degrees are at most one, removing the scalar factors leaves exactly the total formal degree many homogeneous linear forms. No assumption on variable support is required.

theorem homogeneous_product_linear_factors
    (l : List (MvPolynomial σ K × ℕ))
    (hl : ∀ q ∈ l, q.1.IsHomogeneous q.2)
    (hle : ∀ q ∈ l, q.2 ≤ 1) :
    ∃ a : K, ∃ factors : List (MvPolynomial σ K),
      factors.length = (l.map Prod.snd).sum ∧
      (∀ p ∈ factors, p.IsHomogeneous 1) ∧
      (l.map Prod.fst).prod = C a * factors.prod := by
…