ι_f_zero_comp_complex_d — Mathlib

English

The kernel fork associated to the first differential of I.cocomplex is defined as the kernel of d 0 1 with the canonical inclusion ι.

Русский

Кернельная развилка, связанная с первым дифференциалом кокомплексa I, определяется как ядро d_{0 1} с каноническим включением ι.

LaTeX

$$$$\\text{kernelFork}(I) = \\text{KernelFork}(I.cocomplex.d\\;0\\;1)$$$$

Lean4

@[reassoc]
theorem ι_f_zero_comp_complex_d : I.ι.f 0 ≫ I.cocomplex.d 0 1 = 0 := by simp

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