small_span_singleton — Mathlib

English

For any m ∈ M, the span of {m} is finitely generated, hence small.

Русский

Для любого элемента m ∈ M порожденный им подпроизведение спана по одному элементу конечнопорождено, значит малое.

LaTeX

$$$Small(\operatorname{span}_R\{m\})$ for any m ∈ M$$

Lean4

instance small_span_singleton [Small.{u} R] (m : M) : Small.{u} (span R { m }) :=
  FG.small _ (fg_span_singleton _)

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