instFinitaryMatroid

Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

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

English

The E-component of the algebraic independent matroid equals the entire universe when the setup is sufficiently nice.

Русский

Компонента E матроида алгебраической независимости равна всему множеству при подходящих условиях.

LaTeX

$$$ (matroid R A).E = \mathrm{univ}$$$

Lean4

instance : (matroid R A).Finitary where indep_of_forall_finite := algebraicIndependent_of_finite

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

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

Разделы

Аффилиация

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