instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂

English

There is a canonical FunLike structure on the type cocycles₂ A, viewed as functions on G × G with values in A.

Русский

Существует каноническая структура FunLike на множество cocycles₂ A, воспринятая как функции G × G → A.

LaTeX

$$$$ \text{FunLike}(cocycles_2(A)) \, (G \times G) \, A.$$$$

Lean4

instance : FunLike (cocycles₂ A) (G × G) A :=
  ⟨Subtype.val, Subtype.val_injective⟩

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

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

Разделы

Аффилиация

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