opcyclesIsoX₂_hom_inv_id — Mathlib

English

The composition (opcyclesIsoX₂ hf).hom followed by S.pOpcycles equals the identity.

Русский

Состав (S.opcyclesIsoX₂ hf).hom затем S.pOpcycles равен тождественному отображению.

LaTeX

$$$ (S.opcyclesIsoX₂ hf).hom \circ S.pOpcycles = \mathrm{id}_{S.X_2} $$$

Lean4

@[reassoc (attr := simp)]
theorem opcyclesIsoX₂_hom_inv_id (hf : S.f = 0) : (S.opcyclesIsoX₂ hf).hom ≫ S.pOpcycles = 𝟙 _ :=
  (S.opcyclesIsoX₂ hf).hom_inv_id

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