Theorems · Theorem · ring theory

Coalgebra.Repr.eq

∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] {a : A} {ι : Type u_1} (self : Coalgebra.Repr R a ι),
  ∑ i ∈ self.index, self.left i ⊗ₜ[R] self.right i = CoalgebraStruct.comul a

comul a is equal to a finite sum of some pure tensors

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCoalgebraStruct