toHopfAlgEquiv_symm — Mathlib

English

The Hopf algebra equivalence of the opposite of an isomorphism equals the opposite of the Hopf algebra equivalence.

Русский

Эквивалент HopfAlg для симметричной противоположности изоморфизма равен противоположному эквиваленту HopfAlg.

LaTeX

$$$toHopfAlgEquiv( e.\mathrm{symm} ) = (toHopfAlgEquiv e).\mathrm{symm}$$$

Lean4

@[simp]
theorem toHopfAlgEquiv_symm (e : X ≅ Y) : toHopfAlgEquiv e.symm = (toHopfAlgEquiv e).symm :=
  rfl

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