isZero₃_iff — Mathlib

English

In a distinguished triangle, obj3 is zero exactly when mor2 and mor3 vanish; this provides a criterion to test zero-ness via morphisms.

Русский

В отличимом треугольнике obj3 нулевой тогда, когда mor2 и mor3 оба нулевые; критерий для проверки нулевости через морфизмы.

LaTeX

$$$IsZero(T.obj_3) \\iff (T.mor_2 = 0 \\land T.mor_3 = 0)$$$

Lean4

theorem isZero₃_iff : IsZero T.obj₃ ↔ (T.mor₂ = 0 ∧ T.mor₃ = 0) :=
  by
  refine (isZero₂_iff _ (rot_of_distTriang _ hT)).trans ?_
  dsimp
  tauto

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