generators_card

Mathlib.Algebra.Module.SpanRank

URI: https://scilib.ai/kg/mathlib#Submodule.generators_card

English

Let p be a submodule. The cardinality of its chosen generating set equals spanRank(p).

Русский

Пусть p — подмодуль. Кардинал выбранного набора порождающих p равен spanRank(p).

LaTeX

$$$\#(\mathrm{generators}(p)) = \operatorname{spanRank}(p).$$$

Lean4

theorem generators_card (p : Submodule R M) : #(generators p) = spanRank p :=
  (Classical.choose_spec (exists_span_set_card_eq_spanRank p)).1

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

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

Разделы

Аффилиация

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