Theorems · Inductive type · ring theory

Coalgebra.Repr

(R : Type u) →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [CoalgebraStruct R A] → A → Type u_1 → Type (max u_1 v)

A representation of an element a of a coalgebra A is a finite sum of pure tensors ∑ xᵢ ⊗ yᵢ that is equal to comul a.

Defined in

Mathlib.RingTheory.Coalgebra.Basic

Cited by

25 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CommSemiringAddCommMonoidModuleCoalgebraStruct