Theorems · Theorem · ring theory

Coalgebra.comm_comul

∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] [Coalgebra.IsCocomm R A] (a : A),
  (TensorProduct.comm R A A) (CoalgebraStruct.comul a) = CoalgebraStruct.comul a

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCoalgebraCoalgebra.IsCocomm