eqToHom_f

Mathlib.CategoryTheory.DifferentialObject

URI: https://scilib.ai/kg/mathlib#CategoryTheory.DifferentialObject.eqToHom_f

Lean4

@[simp]
theorem eqToHom_f {X Y : DifferentialObject S C} (h : X = Y) : Hom.f (eqToHom h) = eqToHom (congr_arg _ h) :=
  by
  subst h
  rw [eqToHom_refl, eqToHom_refl]
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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