Theorems · Definition · nonassociative algebras

NonUnitalAlgHom.mk.noConfusion

{R : Type u} →
  {S : Type u₁} →
    {inst : Monoid R} →
      {inst_1 : Monoid S} →
        {φ : R →* S} →
          {A : Type v} →
            {B : Type w} →
              {inst_2 : NonUnitalNonAssocSemiring A} →
                {inst_3 : DistribMulAction R A} →
                  {inst_4 : NonUnitalNonAssocSemiring B} →
                    {inst_5 : DistribMulAction S B} →
                      {P : Sort u_1} →
                        {toDistribMulActionHom : A →ₑ+[φ] B} →
                          {map_mul' :
                              ∀ (x y : A),
                                toDistribMulActionHom.toFun (x * y) =
                                  toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y} →
                            {toDistribMulActionHom' : A →ₑ+[φ] B} →
                              {map_mul'' :
                                  ∀ (x y : A),
                                    toDistribMulActionHom'.toFun (x * y) =
                                      toDistribMulActionHom'.toFun x * toDistribMulActionHom'.toFun y} →
                                { toDistribMulActionHom := toDistribMulActionHom, map_mul' := map_mul' } =
                                    { toDistribMulActionHom := toDistribMulActionHom', map_mul' := map_mul'' } →
                                  (toDistribMulActionHom ≍ toDistribMulActionHom' → P) → P

Defined in

Mathlib.Algebra.Algebra.NonUnitalHom

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms