iCyclesIso_inv_hom_id — Mathlib

English

The inverse of iCycles iso composed with iCycles yields the identity on X_i.

Русский

Обратное изоморфизма iCycles при композиции с iCycles даёт тождество на X_i.

LaTeX

$$$$ (K.iCyclesIso\\, i\\, j\\, hj\\, h)^{-1} \\circ K.iCycles i = \\mathrm{Id}_{K.X_i} $$$$

Lean4

@[reassoc (attr := simp)]
theorem iCyclesIso_inv_hom_id : (K.iCyclesIso i j hj h).inv ≫ K.iCycles i = 𝟙 _ :=
  (K.iCyclesIso i j hj h).inv_hom_id

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