ofHasBinaryBiproduct — Mathlib

English

IsZero S.X₂ is equivalent to f = 0 and g = 0.

Русский

IsZero(S.X₂) эквивалентно f = 0 и g = 0.

LaTeX

$$\mathrm{IsZero}(S.X_2) \iff (S.f = 0 \land S.g = 0)$$

Lean4

/-- The obvious splitting of the short complex `X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂`. -/
noncomputable def ofHasBinaryBiproduct (X₁ X₂ : C) [HasBinaryBiproduct X₁ X₂] :
    Splitting (ShortComplex.mk (biprod.inl : X₁ ⟶ _) (biprod.snd : _ ⟶ X₂) (by simp))
    where
  r := biprod.fst
  s := biprod.inr

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