sumLeft_sum

Mathlib.Combinatorics.SimpleGraph.Sum

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Coloring.sumLeft_sum

Lean4

@[simp]
theorem sumLeft_sum (cG : G.Coloring γ) (cH : H.Coloring γ) : (cG.sum cH).sumLeft = cG :=
  rfl

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

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

Разделы

Аффилиация

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