Theorems · Definition · ring theory

CoalgebraStruct.comul

{R : Type u} →
  {A : Type v} →
    {inst : CommSemiring R} →
      {inst_1 : AddCommMonoid A} → {inst_2 : Module R A} → [self : CoalgebraStruct R A] → A →ₗ[R] TensorProduct R A A

The comultiplication of the coalgebra

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

118 results in Mathlib

Foundations

Depth 56 from the axioms, rests on 836 definitions · uses propext, Quot.sound

Assumes

CoalgebraStruct