Theorems · Definition · linear algebra

MultilinearMap.alternatization

{R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N' : Type u_6} →
            [inst_3 : AddCommGroup N'] →
              [inst_4 : Module R N'] →
                {ι : Type u_7} → [Fintype ι] → [DecidableEq ι] → MultilinearMap R (fun x => M) N' →+ M [⋀^ι]→ₗ[R] N'

Produce an AlternatingMap out of a MultilinearMap, by summing over all argument permutations.

Defined in

Mathlib.LinearAlgebra.Alternating.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommGroupModuleFintypeDecidableEq