Theorems · Theorem · ring theory

CoalgHomClass.map_comp_comul

∀ {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), TensorProduct.map ↑f ↑f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ ↑f

Defined in

Mathlib.RingTheory.Coalgebra.Hom

Cited by

4 results in Mathlib

Foundations

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

Assumes

CoalgHomClass