ncard_eq_ncard_of_isBase

Mathlib.Combinatorics.Matroid.Basic

URI: https://scilib.ai/kg/mathlib#Matroid.IsBase.ncard_eq_ncard_of_isBase

← MathLib Explorer

English

If B1 and B2 are bases of M, then B1.ncard = B2.ncard.

Русский

Если B1 и B2 — базы M, то ncard(B1) = ncard(B2).

LaTeX

$$$(hB_1 : M.IsBase B_1) \to (hB_2 : M.IsBase B_2) : B_1.ncard = B_2.ncard$$$

Lean4

theorem ncard_eq_ncard_of_isBase (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) : B₁.ncard = B₂.ncard := by
  rw [ncard_def B₁, hB₁.encard_eq_encard_of_isBase hB₂, ← ncard_def]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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