Theorems · Definition · ring theory

GroupLike.noConfusion

{P : Sort u} →
  {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} →
              {t : GroupLike R A} →
                {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'} →
                            {t' : GroupLike R' A'} →
                              R = R' →
                                A = A' →
                                  inst ≍ inst' →
                                    inst_1 ≍ inst'_1 →
                                      inst_2 ≍ inst'_2 → inst_3 ≍ inst'_3 → t ≍ t' → GroupLike.noConfusionType P t t'

Defined in

Mathlib.RingTheory.Coalgebra.GroupLike

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms