cocycles₂_map_one_fst

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

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

← MathLib Explorer

English

For g ∈ G, f(1,h) = f(1,1) for any cocycle f.

Русский

Для любого кокцикла f выполняется f(1,h) = f(1,1).

LaTeX

$$$$ \\forall f \\in cocycles_2(A), \\forall g \\in G, f(1,g) = f(1,1). $$$$

Lean4

theorem cocycles₂_map_one_fst (f : cocycles₂ A) (g : G) : f (1, g) = f (1, 1) :=
  by
  have := ((mem_cocycles₂_iff f).1 f.2 1 1 g).symm
  simpa only [map_one, Module.End.one_apply, one_mul, add_right_inj, this]

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

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

Разделы

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

Аффилиация

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