Theorems · Theorem · ring theory

Coalgebra.sum_tmul_counit_eq

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

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCoalgebra