mem_span_insert' — Mathlib

English

For a ring, membership in span(insert y s) is equivalent to existence of a such that x + a y ∈ span s.

Русский

Для кольца принадлежность элементa x в span(порождение y s) равносильна существованию a такой, что x + a y ∈ span s.

LaTeX

$$$$ x \in \operatorname{span}(\operatorname{insert} y s) \iff \exists a, \ x + a \cdot y \in \operatorname{span}(s) $$$$

Lean4

theorem mem_span_insert' {s : Set α} {x y} : x ∈ span (insert y s) ↔ ∃ a, x + a * y ∈ span s :=
  Submodule.mem_span_insert'

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