exists_set_linearIndependent — Mathlib

English

For any ring R with HasRankNullity, there exists a subset s ⊆ M such that #s = rank_R M and the inclusion map is linearly independent.

Русский

При HasRankNullity существует подмножество s ⊆ M такое, что #s = rank_R M и включение линейно независимо.

LaTeX

$$$\exists s : Set M,\; \#s = \operatorname{Module.rank} R M \; \land\; \operatorname{LinearIndependent} R (\mathrm{Subtype}.val)$$$

Lean4

theorem exists_set_linearIndependent : ∃ s : Set M, #s = Module.rank R M ∧ LinearIndependent (ι := s) R Subtype.val :=
  HasRankNullity.exists_set_linearIndependent M

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