Theorems · Theorem

CoassocSimps.map_counit_comp_comul_left

∀ {R : Type u_1} {M : Type u_3} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] [inst_5 : Coalgebra R M] (f : M →ₗ[R] M'),
  TensorProduct.map CoalgebraStruct.counit f ∘ₗ CoalgebraStruct.comul =
    TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R M).symm

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites22

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

DFunLike.coeproof · cited by 62,936
Modulestatement and proof · cited by 20,661
RingHom.idstatement and proof · cited by 18,349
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement and proof · cited by 10,215
TensorProductstatement and proof · cited by 2,545
LinearMap.compstatement and proof · cited by 1,642
LinearEquiv.symmstatement and proof · cited by 1,461
LinearEquiv.toLinearMapstatement and proof · cited by 1,171
LinearMap.idstatement and proof · cited by 625
LinearMap.rTensorproof · cited by 266

Cited by1

Results whose statement or proof uses this declaration.

CoassocSimps.map_counit_comp_comul_left_assocproof · cited by 0