Theorems · Theorem · linear algebra

MultilinearMap.snoc_smul

∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
  (m : (i : Fin n) → M i.castSucc) (c : R) (x : M (Fin.last n)), f (Fin.snoc m (c • x)) = c • f (Fin.snoc m x)

In the specific case of multilinear maps on spaces indexed by Fin (n+1), where one can build an element of ∀ (i : Fin (n+1)), M i using cons, one can express directly the multiplicativity of a multilinear map along the first variable.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

0 results in Mathlib

Foundations

Depth 53 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule