d_ofNat

Mathlib.Algebra.Homology.Embedding.Connect

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

English

For natural indices, the connecting differential matches the L-differential: h.d(n_cast, m_cast) = L.d(n,m).

Русский

Для натуральных индексов дифференциал соединения совпадает с L.d: h.d(n_cast,m_cast) = L.d(n,m).

LaTeX

$$@[simp] d_ofNat (n m : ℕ) : h.d n.cast m.cast = L.d n m$$

Lean4

@[simp]
theorem d_ofNat (n m : ℕ) : h.d n m = L.d n m :=
  rfl

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

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

Разделы

Аффилиация

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