opcyclesIso_inv_comp_descOpcycles

English

Inverse iso relation: h.opcyclesIso.inv ≫ S.descOpcycles k hk = h.descQ k hk.

Русский

Обратное отношение изоморфии: h.opcyclesIso.inv ≫ S.descOpcycles k hk = h.descQ k hk.

LaTeX

$$$h.opcyclesIso.inv \\circ S.descOpcycles k hk = h.descQ k hk$$$

Lean4

@[reassoc (attr := simp)]
theorem opcyclesIso_inv_comp_descOpcycles : h.opcyclesIso.inv ≫ S.descOpcycles k hk = h.descQ k hk := by
  simp only [← cancel_epi h.p, p_comp_opcyclesIso_inv_assoc, p_descOpcycles, p_descQ]

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