Theorems · Theorem · ring theory

Coalgebra.coassoc

∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  [self : Coalgebra R A],
  ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul =
    LinearMap.lTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul

The comultiplication is coassociative

Defined in: Mathlib.RingTheory.Coalgebra.Basic
Cited by: 3 results in Mathlib
Foundations: Depth 70 from the axioms · uses propext, Quot.sound
Assumes: Coalgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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.idstatement · cited by 18,349
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement · cited by 10,215
TensorProductstatement · cited by 2,545
LinearMap.compstatement · cited by 1,642
LinearEquiv.toLinearMapstatement · cited by 1,171
LinearMap.rTensorstatement · cited by 266
LinearMap.lTensorstatement · cited by 203
CoalgebraStruct.comulstatement · cited by 118
Coalgebrastatement and proof · cited by 112

Cited by3

Results whose statement or proof uses this declaration.

CoassocSimps.assoc_comp_map_comm_comp_comul_comp_comulproof · cited by 1
Coalgebra.sum_tmul_tmul_eqproof · cited by 1
Coalgebra.coassoc_applyproof · cited by 1