coeff_minpolyDiv_sub_pow_mem_span

English

For all i up to the degree of minpolyDiv R x, the coefficient of minpolyDiv R x at degree natDegree(minpolyDiv R x) − i, minus x^i, lies in the span of lower powers of x over R.

Русский

Для всех i ≤ deg(minpolyDiv R x) скаляльный коэффициент при deg(minpolyDiv R x)−i минполиномMinpolyDiv R x минус x^i лежит в подмодуле, порождаемом степенями x с показателями меньше i.

LaTeX

$$$\text{coeff}(\minpolyDiv\,R\ x)\big( \operatorname{natDegree}(\minpolyDiv\,R\ x) - i \big) - x^i \in \operatorname{Submodule}.span_R( (x^\cdot)''\mathrm{Iio}(i) )$$$

Lean4

theorem coeff_minpolyDiv_sub_pow_mem_span {i} (hi : i ≤ natDegree (minpolyDiv R x)) :
    coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i ∈ Submodule.span R ((x ^ ·) '' Set.Iio i) := by
  induction i with
  | zero => simp [(minpolyDiv_monic hx).leadingCoeff]
  | succ i IH =>
    rw [coeff_minpolyDiv, add_sub_assoc, pow_succ, ← sub_mul, Algebra.algebraMap_eq_smul_one]
    refine add_mem ?_ ?_
    · apply Submodule.smul_mem
      apply Submodule.subset_span
      exact ⟨0, Nat.zero_lt_succ _, pow_zero _⟩
    · rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left (b := 1) hi)]
      apply
        SetLike.le_def.mp ?_
          (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi)) (Submodule.mem_span_singleton_self x))
      rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]
      apply Submodule.span_mono
      rintro _ ⟨j, hj, rfl⟩
      rw [Set.mem_Iio] at hj
      exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ x j⟩

Похожие утверждения