insert_id_rhs

Mathlib.Tactic.CategoryTheory.Coherence

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

Lean4

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

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

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

Разделы

Аффилиация

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