instCoeHomHomObj

Mathlib.CategoryTheory.Galois.Prorepresentability

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCoeHomHomObj

Lean4

instance {A B : PointedGaloisObject F} : Coe (Hom A B) (A.obj ⟶ B.obj) where coe f := f.val

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

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

Разделы

Аффилиация

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