d₁₂_apply_mem_cocycles₂

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupCohomology.d₁₂_apply_mem_cocycles₂

English

For x: G → A, d₁₂(A)(x) ∈ cocycles₂(A).

Русский

Для любой x: G → A выполняется d₁₂(A)(x) ∈ cocycles₂(A).

LaTeX

$$$$ \\forall x: G \\to A, \\ d_{1 2}(A)(x) \\in cocycles_2(A). $$$$

Lean4

theorem d₁₂_apply_mem_cocycles₂ (x : G → A) : d₁₂ A x ∈ cocycles₂ A :=
  d₁₂_comp_d₂₃_apply _ _

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

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

Разделы

Аффилиация

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