Theorems · Theorem

CoassocSimps.coassoc_right

∀ {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.assoc R M' M M).symm ∘ₗ TensorProduct.map f CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul =
    TensorProduct.map (TensorProduct.map f LinearMap.id) LinearMap.id ∘ₗ
      TensorProduct.map CoalgebraStruct.comul LinearMap.id ∘ₗ CoalgebraStruct.comul

Defined in

Mathlib.RingTheory.Coalgebra.CoassocSimps

Cited by

1 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleCoalgebra