eRank_emptyOn

Mathlib.Combinatorics.Matroid.Rank.ENat

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

English

The eRank of the matroid emptyOn α is 0.

Русский

eRank у матроида emptyOn α равен 0.

LaTeX

$$$ (emptyOn\\, \\alpha).eRank = 0 $$$

Lean4

@[simp]
theorem eRank_emptyOn (α : Type*) : (emptyOn α).eRank = 0 := by rw [eRank_eq_zero_iff, emptyOn_ground, loopyOn_empty]

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

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

Разделы

Аффилиация

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