Theorems · Definition · linear algebra

Basis.multilinearMap

{ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommSemiring R] →
      {M : ι → Type u_3} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            {κ : ι → Type u_5} →
              ((i : ι) → Module.Basis (κ i) R (M i)) →
                {ι' : Type u_6} →
                  {N : Type u_7} →
                    [inst_3 : AddCommMonoid N] →
                      [inst_4 : Module R N] →
                        Module.Basis ι' R N →
                          [Finite ι] →
                            [∀ (i : ι), Finite (κ i)] → Module.Basis (((i : ι) → κ i) × ι') R (MultilinearMap R M N)

A basis for multilinear maps given a finite basis on each domain and a basis on the codomain.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basis

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleFiniteFinite