comp_right_eq_zero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem comp_right_eq_zero [IsIso g] : f ≫ g = 0 ↔ f = 0 := by rw [← IsIso.eq_comp_inv, Limits.zero_comp]

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