of_ladder_addEquiv_of_exact' — Mathlib

English

Variant of the previous lemma with reversed quantifiers on exactness.

Русский

Вариант предыдущей леммы с иной конфигурацией точности.

LaTeX

$$$\\text{Exact}(f_{12},f_{23}) \\Rightarrow \\text{Exact}(g_{12},g_{23})$$$

Lean4

theorem of_ladder_addEquiv_of_exact' (comm₁₂ : g₁₂.comp e₁ = AddMonoidHom.comp e₂ f₁₂)
    (comm₂₃ : g₂₃.comp e₂ = AddMonoidHom.comp e₃ f₂₃) (H : Exact g₁₂ g₂₃) : Exact f₁₂ f₂₃ :=
  (iff_of_ladder_addEquiv _ _ _ comm₁₂ comm₂₃).1 H

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