exists_set — Mathlib

English

If M is a free R-module, then there exists a subset S of M that is a basis for M as an R-module.

Русский

Если M является свободным модулем над R, то существует подмножество S ⊆ M, являющееся базисом M над R.

LaTeX

$$$$ \exists S \subseteq M \;\text{such that } \mathrm{Basis}(S,R,M) $$$$

Lean4

theorem exists_set [Free R M] : ∃ S : Set M, Nonempty (Basis S R M) :=
  let ⟨_I, b⟩ := exists_basis R M;
  ⟨Set.range b, ⟨b.reindexRange⟩⟩

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