cyclesIso₀ — Mathlib

English

The 0-cycles of the inhomogeneous chain complex are isomorphic to the underlying A-vector space V.

Русский

Нулевые циклы в неоднородном цепном комплексе изоморфны базовому пространству AV.

LaTeX

$$$\operatorname{cycles} A\; 0 \cong A.V$$$

Lean4

/-- The 0-cycles of the complex of inhomogeneous chains of `A` are isomorphic to `A`. -/
def cyclesIso₀ : cycles A 0 ≅ A.V :=
  (inhomogeneousChains A).iCyclesIso _ 0 (by aesop) (by aesop) ≪≫ chainsIso₀ A

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