boundariesToCycles₂_apply

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupHomology.boundariesToCycles₂_apply

English

Applying the natural inclusion to an element x in B₂(A) preserves its underlying component structure.

Русский

Применение включения к элементу x ∈ B₂(A) сохраняет его первую компоненту (структуру).

LaTeX

$$$\big( boundariesToCycles_2(A)\; x \big)_{1} = x_{1}$$$

Lean4

@[simp]
theorem boundariesToCycles₂_apply (x : boundaries₂ A) : (boundariesToCycles₂ A x).1 = x.1 :=
  rfl

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

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

Разделы

Аффилиация

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