rank_span_finset_le

Mathlib.LinearAlgebra.Dimension.Constructions

URI: https://scilib.ai/kg/mathlib#rank_span_finset_le

English

For a finite set s, rank(span_R (s : Set M)) ≤ card(s).

Русский

Для конечного множества s выполнено: ранг(span_R (s : Set M)) ≤ card(s).

LaTeX

$$$ \\operatorname{Module.rank} R (\\operatorname{span}_R (s : Set M)) \\leq s.card. $$$

Lean4

theorem rank_span_finset_le (s : Finset M) : Module.rank R (span R (s : Set M)) ≤ s.card := by
  simpa using rank_span_le s.toSet

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru