English
If R has decidable equality, then degreeLT(R,n) equals the span of X^k for k = 0,...,n-1.
Русский
Если равенство в R разрешимо, то degreeLT(R,n) равно порождению множества X^k для k = 0,...,n-1.
LaTeX
$$$\operatorname{degreeLT}_R(n) = \operatorname{span}_R\!\{ X^k : 0 \le k < n \}. $$$
Lean4
theorem degreeLT_eq_span_X_pow [DecidableEq R] {n : ℕ} :
degreeLT R n = Submodule.span R ↑((Finset.range n).image fun n => X ^ n : Finset R[X]) :=
by
apply le_antisymm
· intro p hp
replace hp := mem_degreeLT.1 hp
rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
refine Submodule.sum_mem _ fun k hk => ?_
have := WithBot.coe_lt_coe.1 ((Finset.sup_lt_iff <| WithBot.bot_lt_coe n).1 hp k hk)
rw [← C_mul_X_pow_eq_monomial, C_mul']
refine Submodule.smul_mem _ _ (Submodule.subset_span <| by grind)
rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]
intro k hk
apply mem_degreeLT.2
exact lt_of_le_of_lt (degree_X_pow_le _) (WithBot.coe_lt_coe.2 <| Finset.mem_range.1 hk)
