span_range_update_sub_smul — Mathlib

English

Transformation with subtraction in the update leaves the span unchanged.

Русский

Преобразование с вычитанием в обновлении оставляет span неизменным.

LaTeX

$$$\operatorname{span}_R\left(\operatorname{range}(\operatorname{Function.update}(v,j(v_j - r v_i)))\right) = \operatorname{span}_R(\operatorname{range}(v))$$$

Lean4

theorem span_range_update_sub_smul (hij : i ≠ j) (v : ι → M) (r : R) :
    span R (Set.range (Function.update v j (v j - r • v i))) = span R (Set.range v) := by
  rw [sub_eq_add_neg, ← neg_smul, span_range_update_add_smul hij]

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