idealSpan_range_update_divByMonic

English

A variant statement expressing similar span-membership for the coefficients of p.divModByMonicAux hq for monic q, in terms of span powers and p.coeff.

Русский

Вариант формулировки, аналогичной выше, об принадлежности коэффициентов p.divModByMonicAux hq к span-производным и коэффициентам p.

LaTeX

$$$ (p.divModByMonicAux hq).coeff i \\in span(q)^{deg(p)} * span(p) $$$

Lean4

theorem idealSpan_range_update_divByMonic (hij : i ≠ j) (v : ι → R[X]) (hi : (v i).Monic) :
    span (Set.range (Function.update v j (v j %ₘ v i))) = span (Set.range v) := by
  rw [modByMonic_eq_sub_mul_div _ hi, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
    Submodule.span_range_update_sub_smul hij]

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