Theorems · Definition · linear algebra

Finsupp.curryLinearEquiv

{α : Type u_9} →
  {β : Type u_10} →
    (R : Type u_11) →
      {M : Type u_12} →
        [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M

The linear equivalence between α × β →₀ M and α →₀ β →₀ M. This is the LinearEquiv version of Finsupp.curryEquiv.

Defined in

Mathlib.LinearAlgebra.Finsupp.Defs

Cited by

11 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModule