abelianImageToKernel_comp_kernel_ι_comp_cokernel_π

English

The composition abelianImageToKernel ≫ kernel.ι g ≫ cokernel.π f is zero.

Русский

Композиция abelianImageToKernel ∘ kernel.ι(g) ∘ cokernel.π(f) равна нулю.

LaTeX

$$$$ (\\mathrm{abelianImageToKernel} \\; \\ggg \\mathrm{kernel.ι}(g)) \\; \\ggg \\mathrm{cokernel.π}(f) = 0. $$$$

Lean4

@[reassoc]
theorem abelianImageToKernel_comp_kernel_ι_comp_cokernel_π :
    S.abelianImageToKernel ≫ kernel.ι S.g ≫ cokernel.π S.f = 0 := by simp

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