insert_id_lhs

Mathlib.Tactic.CategoryTheory.Coherence

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Coherence.insert_id_lhs

Lean4

theorem insert_id_lhs {C : Type*} [Category C] {X Y : C} (f g : X ⟶ Y) (w : f ≫ 𝟙 _ = g) : f = g := by simpa using w

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

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

Разделы

Аффилиация

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