Theorems · Definition · linear algebra

MultilinearMap.curryFinFinset

(R : Type uR) →
  (M₂ : Type v₂) →
    (M' : Type v') →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M'] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M'] →
              [inst_4 : Module R M₂] →
                {k l n : ℕ} →
                  {s : Finset (Fin n)} →
                    s.card = k →
                      sᶜ.card = l →
                        MultilinearMap R (fun x => M') M₂ ≃ₗ[R]
                          MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)

If s : Finset (Fin n) is a finite set of cardinality k and its complement has cardinality l, then the space of multilinear maps on fun i : Fin n => M' is isomorphic to the space of multilinear maps on fun i : Fin k => M' taking values in the space of multilinear maps on fun i : Fin l => M'.

Defined in

Mathlib.LinearAlgebra.Multilinear.Curry

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModule