mem_cycles₁_of_mem_boundaries₁

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

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

← MathLib Explorer

English

If f ∈ B1(G,A), then f ∈ Z1(G,A).

Русский

Если f ∈ B1(G,A), то f ∈ Z1(G,A).

LaTeX

$$f ∈ B_1(G,A) ⇒ f ∈ Z_1(G,A)$$

Lean4

theorem mem_cycles₁_of_mem_boundaries₁ (f : G →₀ A) (h : f ∈ boundaries₁ A) : f ∈ cycles₁ A :=
  by
  rcases h with ⟨x, rfl⟩
  exact d₂₁_apply_mem_cycles₁ x

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

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

Разделы

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

Аффилиация

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