Theorems · Theorem · ring theory

Coalgebra.Repr.convMul_apply

∀ {R : Type u_1} {A : Type u_3} {C : Type u_5} {ι : Type u_6} [inst : CommSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A] [inst_3 : SMulCommClass R A A]
  [inst_4 : IsScalarTower R A A] [inst_5 : AddCommMonoid C] [inst_6 : Module R C] [inst_7 : CoalgebraStruct R C] {a : C}
  (𝓡 : Coalgebra.Repr R a ι) (f g : WithConv (C →ₗ[R] A)),
  (f * g).ofConv a = ∑ i ∈ 𝓡.index, f.ofConv (𝓡.left i) * g.ofConv (𝓡.right i)

Defined in

Mathlib.RingTheory.Coalgebra.Convolution

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringNonUnitalNonAssocSemiringModuleSMulCommClassIsScalarTowerAddCommMonoidModuleCoalgebraStruct