Theorems · Definition · category theory

CategoryTheory.Iso.toHopfAlgEquiv

{R : Type u} → [inst : CommRing R] → {X Y : HopfAlgCat R} → (X ≅ Y) → X.carrier ≃ₐc[R] Y.carrier

Build a BialgEquiv from an isomorphism in the category HopfAlgCat R.

Defined in

Mathlib.Algebra.Category.HopfAlgCat.Basic

Cited by

4 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Quot.sound

Assumes

CommRing