Theorems · Theorem · ring theory

CoalgHomClass.counit_comp

∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : AddCommMonoid A} {inst_2 : Module R A} {inst_3 : AddCommMonoid B} {inst_4 : Module R B}
  {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B} {inst_7 : FunLike F A B} [self : CoalgHomClass F R A B]
  (f : F), CoalgebraStruct.counit ∘ₗ ↑f = CoalgebraStruct.counit

Defined in

Mathlib.RingTheory.Coalgebra.Hom

Cited by

3 results in Mathlib

Foundations

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

Assumes

CoalgHomClass