removeLoops_isBasis'_eq

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.removeLoops_isBasis'_eq

English

Removing loops does not change the IsBasis' property.

Русский

Удаление петель не изменяет свойство IsBasis'.

LaTeX

$$$M.removeLoops.IsBasis' = M.IsBasis'$$$

Lean4

@[simp]
theorem removeLoops_isBasis'_eq : M.removeLoops.IsBasis' = M.IsBasis' :=
  by
  ext
  simp [IsBasis']

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

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

Разделы

Аффилиация

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