OAI/Algebra/DepthFive/Homogeneity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.isHomogeneous_list_sum line 12

   Source documentation

   Homogeneity is preserved by a list sum, including the empty sum.

   theorem isHomogeneous_list_sum {K : Type u} [CommSemiring K]
       {σ : Type v} {ι : Type w} (l : List ι) (f : ι → MvPolynomial σ K) (d : ℕ)
       (h : ∀ i ∈ l, (f i).IsHomogeneous d) :
       (l.map f).sum.IsHomogeneous d := by
   …

2. theorem OAI.Problem335.isHomogeneous_list_prod line 23

   Source documentation

   A product's formal degree is the sum of its factors' formal degrees.

   theorem isHomogeneous_list_prod {K : Type u} [CommSemiring K]
       {σ : Type v} {ι : Type w} (l : List ι) (f : ι → MvPolynomial σ K) (d : ι → ℕ)
       (h : ∀ i ∈ l, (f i).IsHomogeneous (d i)) :
       (l.map f).prod.IsHomogeneous (l.map d).sum := by
   …

3. theorem OAI.Problem335.d5LeafValue_isHomogeneous line 33
4. theorem OAI.Problem335.bottomValue_isHomogeneous line 39
5. theorem OAI.Problem335.lowerValue_isHomogeneous line 48
6. theorem OAI.Problem335.middleValue_isHomogeneous line 56
7. theorem OAI.Problem335.upperValue_isHomogeneous line 65
8. theorem OAI.Problem335.circuitValue_isHomogeneous line 73