Theorems · Theorem · ring theory

GroupLike.mk.injEq

∀ {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] (val : A) (isGroupLikeElem_val : IsGroupLikeElem R val) (val_1 : A)
  (isGroupLikeElem_val_1 : IsGroupLikeElem R val_1),
  ({ val := val, isGroupLikeElem_val := isGroupLikeElem_val } =
      { val := val_1, isGroupLikeElem_val := isGroupLikeElem_val_1 }) =
    (val = val_1)

Defined in

Mathlib.RingTheory.Coalgebra.GroupLike

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CommSemiringAddCommMonoidModuleCoalgebra