Theorems · Definition · ring theory

CoalgebraStruct.counit

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

The counit of the coalgebra

Defined in: Mathlib.RingTheory.Coalgebra.Basic
Cited by: 108 results in Mathlib
Foundations: Depth 14 from the axioms, rests on 146 definitions · uses no axioms
Assumes: CoalgebraStruct

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement · cited by 10,215
CoalgebraStructstatement and proof · cited by 230

Cited by139

Results whose statement or proof uses this declaration.

Bialgebra.counitAlgHomproof · cited by 23
IsGroupLikeElem.counit_eq_onestatement · cited by 9
Bialgebra.counit_onestatement · cited by 6
AddMonoidAlgebra.counit_singlestatement · cited by 5
Coalgebra.rTensor_counit_comp_comulstatement · cited by 4
Finsupp.counit_singlestatement and proof · cited by 4
CoalgHomClass.counit_compstatement · cited by 3
Coalgebra.counitCoalgHomproof · cited by 3
Coalgebra.lTensor_counit_comp_comulstatement · cited by 3
HopfAlgebra.sum_antipode_mul_eq_algebraMap_counitstatement and proof · cited by 3
HopfAlgebra.sum_mul_antipode_eq_algebraMap_counitstatement and proof · cited by 3
MonoidAlgebra.counit_singlestatement · cited by 3