isIsoZeroSelfEquivIsoZero — Mathlib

English

A zero endomorphism 0: X → X corresponds to the isomorphism X ≅ 0.

Русский

Нулевой эндоморфизм 0: X → X соответствует изоморфизму X ≅ 0.

LaTeX

$$$IsIso(0:X\to X) \iff X\cong 0$$$

Lean4

/-- A zero morphism `0 : X ⟶ X` is an isomorphism if and only if
`X` is isomorphic to the zero object.
-/
def isIsoZeroSelfEquivIsoZero (X : C) : IsIso (0 : X ⟶ X) ≃ (X ≅ 0) :=
  (isIsoZeroEquivIsoZero X X).trans subsingletonProdSelfEquiv

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