toHopfAlgIso_trans — Mathlib

English

The HopfAlgIso associated to the composition of isomorphisms is the composition of the corresponding HopfAlgIsos.

Русский

Изоморфия HopfAlg, соответствующая композиции изоморфизмов, равна композиции соответствующих HopfAlgIso.

LaTeX

$$$$ toHopfAlgIso(e \\circ f) = toHopfAlgIso(e) \\;\\text{trans}\\; toHopfAlgIso(f). $$$$

Lean4

@[simp]
theorem toHopfAlgIso_trans (e : X ≃ₐc[R] Y) (f : Y ≃ₐc[R] Z) :
    toHopfAlgIso (e.trans f) = toHopfAlgIso e ≪≫ toHopfAlgIso f :=
  rfl

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