span_singleton_le_iff_mem — Mathlib

English

The span of a singleton is contained in any ideal if and only if the element is in that ideal.

Русский

Покрытие одиночного элемента содержится в любом идеале тогда и только тогда, когда элемент принадлежит этому идеалу.

LaTeX

$$$\\operatorname{span}(\\{x\\}) \\le I \\iff x \\in I$$$

Lean4

theorem span_singleton_le_iff_mem {x : α} : span { x } ≤ I ↔ x ∈ I :=
  Submodule.span_singleton_le_iff_mem _ _

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