span — Mathlib

English

The ideal generated by a subset s is defined as the smallest submodule span that contains s; in particular, it coincides with the submodule span of s.

Русский

Идеал, порожденный подмножеством s, определяется как наименьшее подмодульное множество, содержащее s; следовательно, он совпадает с порожденным подмодулем span(s).

LaTeX

$$$\\operatorname{span}(s) = \\operatorname{Submodule.span}_{\\alpha}(s)$$$

Lean4

/-- The ideal generated by a subset of a ring -/
def span (s : Set α) : Ideal α :=
  Submodule.span α s

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