comm

Mathlib.Algebra.Homology.Embedding.HomEquiv

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.homRestrict.comm

Lean4

@[reassoc (attr := simp)]
theorem comm (i j : ι) : f ψ i ≫ L.d i j = K.d (e.f i) (e.f j) ≫ f ψ j :=
  by
  dsimp [f]
  simp only [assoc, ← ψ.comm_assoc, L.extend_d_eq e rfl rfl, Iso.inv_hom_id, comp_id]

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

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

Разделы

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

Аффилиация

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