exists_fin — Mathlib

English

If M is a finite R-module, there exists a finite index n and a function s: Fin n → M such that span_R(range s) = ⊤.

Русский

Если M — конечный R-модуль, то существует конечное множество порождающих, задаваемое функцией s: Fin n → M, для которого span_R(range s) = ⊤.

LaTeX

$$$\exists n \; \exists s : Fin n \to M, \ \operatorname{span}_R(\operatorname{range} s) = \top$$$

Lean4

/-- See also `Module.Finite.exists_fin'`. -/
theorem exists_fin [Module.Finite R M] : ∃ (n : ℕ) (s : Fin n → M), Submodule.span R (range s) = ⊤ :=
  Submodule.fg_iff_exists_fin_generating_family.mp fg_top

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