Theorems · Definition · group theory

MulSemiringActionHom.mk.noConfusion

{M : Type u_1} →
  {inst : Monoid M} →
    {N : Type u_2} →
      {inst_1 : Monoid N} →
        {φ : M →* N} →
          {R : Type u_10} →
            {inst_2 : Semiring R} →
              {inst_3 : MulSemiringAction M R} →
                {S : Type u_12} →
                  {inst_4 : Semiring S} →
                    {inst_5 : MulSemiringAction N S} →
                      {P : Sort u} →
                        {toDistribMulActionHom : R →ₑ+[φ] S} →
                          {map_one' : toDistribMulActionHom.toFun 1 = 1} →
                            {map_mul' :
                                ∀ (x y : R),
                                  toDistribMulActionHom.toFun (x * y) =
                                    toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y} →
                              {toDistribMulActionHom' : R →ₑ+[φ] S} →
                                {map_one'' : toDistribMulActionHom'.toFun 1 = 1} →
                                  {map_mul'' :
                                      ∀ (x y : R),
                                        toDistribMulActionHom'.toFun (x * y) =
                                          toDistribMulActionHom'.toFun x * toDistribMulActionHom'.toFun y} →
                                    { toDistribMulActionHom := toDistribMulActionHom, map_one' := map_one',
                                          map_mul' := map_mul' } =
                                        { toDistribMulActionHom := toDistribMulActionHom', map_one' := map_one'',
                                          map_mul' := map_mul'' } →
                                      (toDistribMulActionHom ≍ toDistribMulActionHom' → P) → P

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms