matroid_cRank_eq

Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

URI: https://scilib.ai/kg/mathlib#AlgebraicIndependent.matroid_cRank_eq

English

The cRank of the independent matroid equals the transcendence degree of the extension.

Русский

cRank матроида независимости равен трансцендентному размеру расширения.

LaTeX

$$$ (matroid R A).cRank = \operatorname{trdeg} R A$$$

Lean4

theorem matroid_cRank_eq : (matroid R A).cRank = trdeg R A :=
  (trdeg_eq_iSup_cardinalMk_isTranscendenceBasis _).symm

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

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

Разделы

Аффилиация

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