Theorems · Definition · ring theory

GroupLike.val

{R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [inst_3 : Coalgebra R A] → GroupLike R A → A

The underlying element of a group-like element.

Defined in

Mathlib.RingTheory.Coalgebra.GroupLike

Cited by

16 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CommSemiringAddCommMonoidModuleCoalgebra