iCycles_mk — Mathlib

English

The inclusion of Z_m into X_m sends cyclesMk(m,n,h,f,hf) to the original f; i.e., iCycles A m (cyclesMk m n h f hf) = f.

Русский

Вложение Z_m в X_m переводит cyclesMk(m,n,h,f,hf) в исходное f; то есть iCycles A m (cyclesMk m n h f hf) = f.

LaTeX

$$iCycles(A,m) (cyclesMk(m,n,h,f,hf)) = f$$

Lean4

theorem iCycles_mk {m n : ℕ} (h : (ComplexShape.down ℕ).next m = n) (f : (Fin m → G) →₀ A)
    (hf : (inhomogeneousChains A).d m n f = 0) : iCycles A m (cyclesMk m n h f hf) = f := by
  exact (inhomogeneousChains A).i_cyclesMk f n h hf

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