single_one_mem_boundaries₁

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupHomology.single_one_mem_boundaries₁

English

The element single 1 a lies in B1(A) for any a ∈ A.

Русский

Элемент single 1 a принадлежит B1(A) для любого a ∈ A.

LaTeX

$$single 1 a ∈ B_1(G,A)$$

Lean4

theorem single_one_mem_boundaries₁ (a : A) : single 1 a ∈ boundaries₁ A :=
  by
  use single (1, 1) a
  simp [d₂₁]

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

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

Разделы

Аффилиация

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