kernelZeroIsoSource_inv — Mathlib

English

The inverse of the kernelZeroIsoSource is the lift of the zero morphism with identity domain.

Русский

Обратный к kernelZeroIsoSource равен лифту нулевого морфизма с тождественным доменом.

LaTeX

$$$\\operatorname{kernelZeroIsoSource}.inv = \\operatorname{kernel.lift}(0:X\\to Y,\\; \\mathrm{id}_X,\\; \\text{proof})$$$

Lean4

@[simp]
theorem kernelZeroIsoSource_inv : kernelZeroIsoSource.inv = kernel.lift (0 : X ⟶ Y) (𝟙 X) (by simp) :=
  by
  ext
  simp [kernelZeroIsoSource]

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