Theorems · Theorem · ring theory

BialgEquiv.mk.inj

∀ {R : Type u} {inst : CommSemiring R} {A : Type v} {B : Type w} {inst_1 : Semiring A} {inst_2 : Semiring B}
  {inst_3 : Algebra R A} {inst_4 : Algebra R B} {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B}
  {toCoalgEquiv : A ≃ₗc[R] B}
  {map_mul' : ∀ (x y : A), toCoalgEquiv.toFun (x * y) = toCoalgEquiv.toFun x * toCoalgEquiv.toFun y}
  {toCoalgEquiv_1 : A ≃ₗc[R] B}
  {map_mul'_1 : ∀ (x y : A), toCoalgEquiv_1.toFun (x * y) = toCoalgEquiv_1.toFun x * toCoalgEquiv_1.toFun y},
  { toCoalgEquiv := toCoalgEquiv, map_mul' := map_mul' } = { toCoalgEquiv := toCoalgEquiv_1, map_mul' := map_mul'_1 } →
    toCoalgEquiv = toCoalgEquiv_1

Defined in

Mathlib.RingTheory.Bialgebra.Equiv

Cited by

1 results in Mathlib

Foundations

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