Theorems · Definition · group theory

MulActionHom.prodMap

{M : Type u_1} →
  {N : Type u_2} →
    {α : Type u_3} →
      {β : Type u_4} →
        {γ : Type u_5} →
          {δ : Type u_6} →
            [inst : SMul M α] →
              [inst_1 : SMul M β] →
                [inst_2 : SMul N γ] → [inst_3 : SMul N δ] → {σ : M → N} → (α →ₑ[σ] γ) → (β →ₑ[σ] δ) → α × β →ₑ[σ] γ × δ

If f and g are equivariant maps, then so is (x, y) ↦ (f x, g y).

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

SMulSMulSMulSMul