pseudoZero_iff — Mathlib

English

A pseudoelement is zero iff its underlying arrow is the zero morphism.

Русский

Псевдоэлемент равен нулю тогда и только тогда, когда соответствующий ему стрелка равна нулю.

LaTeX

$$$a = 0 \\iff a.hom = 0$$$

Lean4

/-- The pseudoelement induced by an arrow is zero precisely when that arrow is zero. -/
theorem pseudoZero_iff {P : C} (a : Over P) : a = (0 : P) ↔ a.hom = 0 :=
  by
  rw [← pseudoZero_aux P a]
  exact Quotient.eq'

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