mk_d_2_1 — Mathlib

English

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

Русский

Аналогично, дифференциал в степени (2,1) равен d1.

LaTeX

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

Lean4

@[simp]
theorem mk_d_2_1 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁ :=
  by
  change ite (2 = 1 + 1) (𝟙 X₂ ≫ d₁) 0 = d₁
  rw [if_pos rfl, Category.id_comp]
    -- TODO simp lemmas for the inductive steps? It's not entirely clear that they are needed.

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