span_of_finite — Mathlib

English

The submodule generated by a finite set is finite.

Русский

Подмодуль, порожденный конечным множеством элементов, конечен.

LaTeX

$$$\\forall A\\subseteq M\\text{ finite},\\; \\text{Module.Finite } R (\\mathrm{span}_R(A))$$$

Lean4

/-- The submodule generated by a finite set is `R`-finite. -/
theorem span_of_finite {A : Set M} (hA : Set.Finite A) : Module.Finite R (Submodule.span R A) :=
  ⟨(Submodule.fg_top _).mpr ⟨hA.toFinset, hA.coe_toFinset.symm ▸ rfl⟩⟩

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