English
For a decidable R, degreeLT(R,n) equals the span of X^k for k < n.
Русский
При разрешимости равенства в R, degreeLT(R,n) эквивалентен порождению X^k для k < n.
LaTeX
$$$\operatorname{degreeLT}_R(n) = \operatorname{span}_R\{ X^k : k < n \}. $$$
Lean4
theorem geom_sum {P : R[X]} (hP : P.Monic) (hdeg : 0 < P.natDegree) {n : ℕ} (hn : n ≠ 0) :
(∑ i ∈ range n, P ^ i).Monic := by
nontriviality R
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
rw [geom_sum_succ']
refine (hP.pow _).add_of_left ?_
refine lt_of_le_of_lt (degree_sum_le _ _) ?_
rw [Finset.sup_lt_iff]
· simp only [Finset.mem_range, degree_eq_natDegree (hP.pow _).ne_zero]
simp only [Nat.cast_lt, hP.natDegree_pow]
intro k
exact nsmul_lt_nsmul_left hdeg
· rw [bot_lt_iff_ne_bot, Ne, degree_eq_bot]
exact (hP.pow _).ne_zero
