span_insert_zero — Mathlib

English

Inserting zero into a set does not change its span: span R (insert 0 s) = span R s.

Русский

Добавление нуля к множеству не изменяет его span: span R (insert 0 s) = span R s.

LaTeX

$$$ \operatorname{span} R (\operatorname{insert}(0 : M)\, s) = \operatorname{span} R s. $$$

Lean4

@[simp]
theorem span_insert_zero : span R (insert (0 : M) s) = span R s :=
  by
  refine le_antisymm ?_ (Submodule.span_mono (Set.subset_insert 0 s))
  rw [span_le, Set.insert_subset_iff]
  exact ⟨by simp only [SetLike.mem_coe, Submodule.zero_mem], Submodule.subset_span⟩

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