English
The span of the coefficients of minpolyDiv R x equals the submodule generated by x over R, i.e., the adjoin of x inside the R-algebra sense.
Русский
Порождение коэффициентов minpolyDiv R x совпадает с подмодулем, порождаемым x над R, то есть адjoin R {x}.
LaTeX
$$$\operatorname{span}_R\{ \operatorname{coeff}(\minpolyDiv R x) \} = \operatorname{toSubmodule}(\operatorname{Algebra.adjoin}_R\{x\})$$$
Lean4
theorem span_coeff_minpolyDiv :
Submodule.span R (Set.range (coeff (minpolyDiv R x))) = Subalgebra.toSubmodule (Algebra.adjoin R { x }) :=
by
nontriviality S
classical
apply le_antisymm
· rw [Submodule.span_le]
rintro _ ⟨i, rfl⟩
apply coeff_minpolyDiv_mem_adjoin
· rw [← Submodule.span_range_natDegree_eq_adjoin (minpoly.monic hx) (minpoly.aeval _ _), Submodule.span_le]
simp only [Finset.coe_image, Finset.coe_range, Set.image_subset_iff]
intro i
induction i using Nat.strongRecOn with
| ind i hi => ?_
intro hi'
have :
coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) ∈ Submodule.span R (Set.range (coeff (minpolyDiv R x))) :=
Submodule.subset_span (Set.mem_range_self _)
rw [Set.mem_preimage, SetLike.mem_coe, ← Submodule.sub_mem_iff_right _ this]
refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span hx ?_)
· rw [Submodule.span_le, Set.image_subset_iff]
intro j (hj : j < i)
exact hi j hj (lt_trans hj hi')
· rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at hi'
