cyclesMk₁_eq — Mathlib

English

A compatibility equality for cyclesMk at level 1 with the inv of chainsIso₁.

Русский

Совпадение cyclesMk на уровне 1 со обратной связью от chainsIso₁.

LaTeX

$$$ (cyclesMk\ 1\ 0\ (by simp))\ ((chainsIso_1 A)$.inv x) = (\text{isoCycles}_1 A)^{-1} x$$

Lean4

theorem cyclesMk₁_eq (x : cycles₁ A) : cyclesMk 1 0 (by simp) ((chainsIso₁ A).inv x) (by simp) = (isoCycles₁ A).inv x :=
  (ModuleCat.mono_iff_injective <| iCycles A 1).1 inferInstance <|
    by
    rw [iCycles_mk]
    simp only [ChainComplex.of_x, isoCycles₁_inv_comp_iCycles_apply]
    rfl

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