mk_d_1_0 — Mathlib

English

In the mk construction, the differential in degree (1,0) equals d0: (mk X0 X1 X2 d0 d1 s succ).d 1 0 = d0.

Русский

В конструкторе mk дифференциал в степени (1,0) равен d0.

LaTeX

$$$$(\\mathrm{mk}\\ X_0 X_1 X_2\ \ d_0\ d_1\ s\ succ).d_{1 0} = d_0$$$$

Lean4

@[simp]
theorem mk_d_1_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀ :=
  by
  change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀
  rw [if_pos rfl, Category.id_comp]

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