Theorems · Inductive type · ring theory

IsGroupLikeElem

(R : Type u_2) →
  {A : Type u_3} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [Coalgebra R A] → A → Prop

A group-like element in a coalgebra is an element a such that ε(a) = 1 and Δ(a) = a ⊗ₜ a, where ε and Δ are the counit and comultiplication respectively.

Defined in

Mathlib.RingTheory.Coalgebra.GroupLike

Cited by

39 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CommSemiringAddCommMonoidModuleCoalgebra