Theorems · Definition · ring theory

NonUnitalStarAlgHom.noConfusion

{P : Sort u} →
  {R : Type u_1} →
    {A : Type u_2} →
      {B : Type u_3} →
        {inst : Monoid R} →
          {inst_1 : NonUnitalNonAssocSemiring A} →
            {inst_2 : DistribMulAction R A} →
              {inst_3 : Star A} →
                {inst_4 : NonUnitalNonAssocSemiring B} →
                  {inst_5 : DistribMulAction R B} →
                    {inst_6 : Star B} →
                      {t : A →⋆ₙₐ[R] B} →
                        {R' : Type u_1} →
                          {A' : Type u_2} →
                            {B' : Type u_3} →
                              {inst' : Monoid R'} →
                                {inst'_1 : NonUnitalNonAssocSemiring A'} →
                                  {inst'_2 : DistribMulAction R' A'} →
                                    {inst'_3 : Star A'} →
                                      {inst'_4 : NonUnitalNonAssocSemiring B'} →
                                        {inst'_5 : DistribMulAction R' B'} →
                                          {inst'_6 : Star B'} →
                                            {t' : A' →⋆ₙₐ[R'] B'} →
                                              R = R' →
                                                A = A' →
                                                  B = B' →
                                                    inst ≍ inst' →
                                                      inst_1 ≍ inst'_1 →
                                                        inst_2 ≍ inst'_2 →
                                                          inst_3 ≍ inst'_3 →
                                                            inst_4 ≍ inst'_4 →
                                                              inst_5 ≍ inst'_5 →
                                                                inst_6 ≍ inst'_6 →
                                                                  t ≍ t' → NonUnitalStarAlgHom.noConfusionType P t t'

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms