Theorems · Theorem · ring theory

GroupLike.mk.inj

∀ {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

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms