boundaries₂_le_cycles₂ — Mathlib

English

In a group representation, every 2-boundary is automatically a 2-cycle; i.e. the boundary subgroup B₂(A) is contained in the cycle subgroup Z₂(A).

Русский

В группе с действием на модуле каждый 2-границе принадлежит также к 2-циклами; то есть B₂(A) ⊆ Z₂(A).

LaTeX

$$$B_2(G,A) \le Z_2(G,A)$$$

Lean4

theorem boundaries₂_le_cycles₂ : boundaries₂ A ≤ cycles₂ A :=
  mem_cycles₂_of_mem_boundaries₂

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