English
Example: in k[x] with grading by degree, the span of homogeneous polynomials of fixed degree is homogeneous.
Русский
Пример: в k[x] с градацией по степеням, порожденная множество однородных многочленов фиксированной степени является однородной.
LaTeX
$$Ideal.IsHomogeneous 𝒜 (Ideal.span {f ∈ k[x] | deg f = d})$$
Lean4
theorem homogeneous_span (s : Set A) (h : ∀ x ∈ s, SetLike.IsHomogeneousElem 𝒜 x) : (Ideal.span s).IsHomogeneous 𝒜 :=
by
rintro i r hr
rw [Ideal.span, Finsupp.span_eq_range_linearCombination] at hr
rw [LinearMap.mem_range] at hr
obtain ⟨s, rfl⟩ := hr
rw [Finsupp.linearCombination_apply, Finsupp.sum, decompose_sum, DFinsupp.finset_sum_apply,
AddSubmonoidClass.coe_finset_sum]
refine Ideal.sum_mem _ ?_
rintro z hz1
rw [smul_eq_mul]
refine Ideal.mul_homogeneous_element_mem_of_mem 𝒜 (s z) z ?_ ?_ i
· rcases z with ⟨z, hz2⟩
apply h _ hz2
· exact Ideal.subset_span z.2
