comp_left_eq_zero — Mathlib

English

Let C be a preadditive category. If f is an isomorphism and f : P → Q, g : Q → R are morphisms, then f ≫ g = 0 if and only if g = 0.

Русский

Пусть C — преддобавительная категория. Если f: P → Q является изоморфизмом и g: Q → R — морфизм, то f ≫ g = 0 тогда и только тогда, когда g = 0.

LaTeX

$$$\forall f: P \to Q, \forall g: Q \to R,\ [\mathrm{IsIso}(f)] \Rightarrow \bigl(f \circ g = 0 \iff g = 0\bigr)$$$

Lean4

@[simp]
theorem comp_left_eq_zero [IsIso f] : f ≫ g = 0 ↔ g = 0 := by rw [← IsIso.eq_inv_comp, Limits.comp_zero]

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