XIso

Mathlib.Algebra.Homology.Embedding.Extend

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.extend.XIso

Lean4

/-- The isomorphism `X K i ≅ K.X j` when `i = some j`. -/
noncomputable def XIso {i : Option ι} {j : ι} (hj : i = some j) : X K i ≅ K.X j :=
  eqToIso (by subst hj; rfl)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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