boundariesToCycles₁_apply — Mathlib

English

The inclusion map from B1(G,A) to Z1(G,A) respects underlying elements; it sends f ∈ B1 to itself when viewed as a cycle.

Русский

Включение из B1(G,A) в Z1(G,A) сохраняет подлежащий элемент; f отображается как f в цикле.

LaTeX

$$boundariesToCycles_1 : B_1(G,A) →ₗ[k] Z_1(G,A) ; (boundariesToCycles₁ A x).1 = x.1$$

Lean4

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

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