finrank_span_finset_eq_card — Mathlib

English

Let R be a semiring and M an R-module. If a finite subset s of M is linearly independent, then the dimension of the span of s equals the cardinality of s.

Русский

Пусть R — полускольное кольцо, M — модуль над R. Если s — конечное подмножество M, линейно независимое, то размерность пространства, порождаемого s, равна мощности множества s.

LaTeX

$$$\operatorname{LinearIndepOn}_R(\operatorname{id}_M)(s) \Rightarrow \operatorname{finrank}_R(\operatorname{span}_R(s)) = |s|$, where $s$ is a finite subset of $M$.$$

Lean4

theorem finrank_span_finset_eq_card {s : Finset M} (hs : LinearIndepOn R id (s : Set M)) :
    finrank R (span R (s : Set M)) = s.card :=
  by
  convert finrank_span_set_eq_card (s := (s : Set M)) hs
  ext
  simp

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