English
The degreeLT(n) submodule equals the span of X^i for i in 0,...,n-1 (finite range).
Русский
Подмодуль degreeLT(n) совпадает с порождением {X^i} для i = 0,...,n-1 (конечный диапазон).
LaTeX
$$$\operatorname{degreeLT}_R(n) = \operatorname{span}_R\big(\{ X^i : 0 \le i < n \}\big).$$$
Lean4
/-- The first `n` coefficients on `degreeLT n` form a linear equivalence with `Fin n → R`. -/
def degreeLTEquiv (R) [Semiring R] (n : ℕ) : degreeLT R n ≃ₗ[R] Fin n → R
where
toFun p n := (↑p : R[X]).coeff n
invFun
f :=
⟨∑ i : Fin n, monomial i (f i),
(degreeLT R n).sum_mem fun i _ =>
mem_degreeLT.mpr (lt_of_le_of_lt (degree_monomial_le i (f i)) (WithBot.coe_lt_coe.mpr i.is_lt))⟩
map_add' p
q := by
ext
dsimp
rw [coeff_add]
map_smul' x
p := by
ext
dsimp
rw [coeff_smul]
rfl
left_inv := by
rintro ⟨p, hp⟩
ext1
simp only
by_cases hp0 : p = 0
· subst hp0
simp only [coeff_zero, LinearMap.map_zero, Finset.sum_const_zero]
rw [mem_degreeLT, degree_eq_natDegree hp0, Nat.cast_lt] at hp
conv_rhs => rw [p.as_sum_range' n hp, ← Fin.sum_univ_eq_sum_range]
right_inv
f := by
ext i
simp only [finset_sum_coeff]
rw [Finset.sum_eq_single i, coeff_monomial, if_pos rfl]
· rintro j - hji
rw [coeff_monomial, if_neg]
rwa [← Fin.ext_iff]
· intro h
exact (h (Finset.mem_univ _)).elim
