Theorems · Theorem · ring theory

BialgEquiv.mk.sizeOf_spec

∀ {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]
  [inst_7 : SizeOf R] [inst_8 : SizeOf A] [inst_9 : SizeOf B] (toCoalgEquiv : A ≃ₗc[R] B)
  (map_mul' : ∀ (x y : A), toCoalgEquiv.toFun (x * y) = toCoalgEquiv.toFun x * toCoalgEquiv.toFun y),
  sizeOf { toCoalgEquiv := toCoalgEquiv, map_mul' := map_mul' } = 1 + sizeOf toCoalgEquiv

Defined in

Mathlib.RingTheory.Bialgebra.Equiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringAlgebraAlgebraCoalgebraStructCoalgebraStructSizeOfSizeOfSizeOf