Theorems · Definition · ring theory

Coalgebra.counitCoalgHom

(R : Type u) →
  (A : Type v) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [inst_3 : Coalgebra R A] → A →ₗc[R] R

The counit of a coalgebra as a CoalgHom.

Defined in: Mathlib.RingTheory.Coalgebra.Hom
Cited by: 3 results in Mathlib
Foundations: Depth 73 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring AddCommMonoid Module Coalgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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.idproof · cited by 18,349
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
LinearMapproof · cited by 10,215
Coalgebrastatement and proof · cited by 112
CoalgebraStruct.counitproof · cited by 108
CoalgHomstatement · cited by 105

Cited by4

Results whose statement or proof uses this declaration.

Bialgebra.counitBialgHomproof · cited by 4
Bialgebra.counitBialgHom_toCoalgHomstatement · cited by 0
Coalgebra.counitCoalgHom_applystatement · cited by 0
Coalgebra.counitCoalgHom_toLinearMapstatement · cited by 0