eRk_ground

Mathlib.Combinatorics.Matroid.Rank.ENat

URI: https://scilib.ai/kg/mathlib#Matroid.eRk_ground

English

The value of eRk on the ground equals the eRank of the matroid.

Русский

Значение eRk на грунте равно eRank матроидa.

LaTeX

$$$ M.eRk(M.E) = M.eRank $$$

Lean4

@[simp]
theorem eRk_ground (M : Matroid α) : M.eRk M.E = M.eRank :=
  M.eRank_def.symm

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

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

Разделы

Аффилиация

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