mk_eq

Mathlib.Tactic.CategoryTheory.Coherence.Basic

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.BicategoryLike.mk_eq

Lean4

theorem mk_eq {α : Type _} (a b a' b' : α) (ha : a = a') (hb : b = b') (h : a' = b') : a = b := by simp [h, ha, hb]

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

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

Разделы

Аффилиация

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