d_negSucc

Mathlib.Algebra.Homology.Embedding.Connect

URI: https://scilib.ai/kg/mathlib#CochainComplex.ConnectData.d_negSucc

English

Equivalence of h.d on casts: h.d n.cast m.cast = L.d n m.

Русский

Сходимость: h.d на приведения к cast равна L.d.

LaTeX

$$Eq (h.d n.cast m.cast) (L.d n m)$$

Lean4

@[simp]
theorem d_negSucc (n m : ℕ) : h.d (.negSucc n) (.negSucc m) = K.d n m := by simp [d]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru