Theorems · Definition · ring theory

GroupLike.mk.noConfusion

{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} →
            {P : Sort u} →
              {val : A} →
                {isGroupLikeElem_val : IsGroupLikeElem R val} →
                  {val' : A} →
                    {isGroupLikeElem_val' : IsGroupLikeElem R val'} →
                      { val := val, isGroupLikeElem_val := isGroupLikeElem_val } =
                          { val := val', isGroupLikeElem_val := isGroupLikeElem_val' } →
                        (val ≍ val' → P) → P

Defined in

Mathlib.RingTheory.Coalgebra.GroupLike

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms