sumRight_sum

Mathlib.Combinatorics.SimpleGraph.Sum

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

Lean4

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

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

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

Разделы

Аффилиация

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