submodule_span_eq — Mathlib

English

The submodule generated by a set s is equal to the ideal generated by s; i.e., the two notions coincide when viewed as objects in a ring.

Русский

Подмодуль, порожденный множеством s, равен порождению идеала от s; то есть две концепции совпадают в кольце.

LaTeX

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

Lean4

@[simp]
theorem submodule_span_eq {s : Set α} : Submodule.span α s = Ideal.span s :=
  rfl

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