Theorems · Theorem · category theory

CommHopfAlgCat.isoEquivBialgEquiv_apply

∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : HopfAlgebra R X] [inst_3 : CommRing Y]
  [inst_4 : HopfAlgebra R Y]
  (i : { X := X, commRing := inst_1, hopfAlgebra := inst_2 } ≅ { X := Y, commRing := inst_3, hopfAlgebra := inst_4 }),
  CommHopfAlgCat.isoEquivBialgEquiv i = CommHopfAlgCat.ofIso i

Defined in

Mathlib.Algebra.Category.CommHopfAlgCat

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingHopfAlgebraCommRingHopfAlgebra