Theorems · Theorem · ring theory

Coalgebra.sum_tmul_tmul_eq

∀ {R : Type u} {A : Type v} {ι : Type u_1} {κ : ι → Type u_2} {Λ : ι → Type u_3} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] [inst_3 : Coalgebra R A] {a : A} (repr : Coalgebra.Repr R a ι)
  (a₁ : (i : ι) → Coalgebra.Repr R (repr.left i) (κ i)) (a₂ : (i : ι) → Coalgebra.Repr R (repr.right i) (Λ i)),
  ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j)

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCoalgebra