Theorems · Theorem · ring theory

Coalgebra.lTensor_counit_comp_comul

∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  [self : Coalgebra R A],
  LinearMap.lTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul = (TensorProduct.mk R A R).flip 1

The counit satisfies the right counitality law

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

Coalgebra