English
If R has decidable equality, then degreeLT(R,n) is exactly the span of the polynomials X^0, X^1, ..., X^{n-1}.
Русский
Пусть в R есть допустимость различения элементов. Тогда degreeLT(R,n) равен порождению подмодуля над R на мономами X^0, X^1, ..., X^{n-1}.
LaTeX
$$$\operatorname{degreeLT}_R(n) = \operatorname{span}_R\!\{ X^0, X^1, \dots, X^{n-1} \}.$$$
Lean4
theorem degreeLE_eq_span_X_pow [DecidableEq R] {n : ℕ} :
degreeLE R n = Submodule.span R ↑((Finset.range (n + 1)).image fun n => (X : R[X]) ^ n) :=
by
apply le_antisymm
· intro p hp
replace hp := mem_degreeLE.1 hp
rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
refine Submodule.sum_mem _ fun k hk => ?_
have := WithBot.coe_le_coe.1 (Finset.sup_le_iff.1 hp k hk)
rw [← C_mul_X_pow_eq_monomial, C_mul']
refine
Submodule.smul_mem _ _
(Submodule.subset_span <|
Finset.mem_coe.2 <| Finset.mem_image.2 ⟨_, Finset.mem_range.2 (Nat.lt_succ_of_le this), rfl⟩)
rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]
intro k hk
apply mem_degreeLE.2
exact (degree_X_pow_le _).trans (WithBot.coe_le_coe.2 <| Nat.le_of_lt_succ <| Finset.mem_range.1 hk)
